/-
Copyright (c) 2019 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Yaël Dillies
-/
import Mathlib.Algebra.Module.BigOperators
import Mathlib.Data.Finset.NoncommProd
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Int.ModEq
import Mathlib.GroupTheory.Perm.List
import Mathlib.GroupTheory.Perm.Sign
import Mathlib.Logic.Equiv.Fintype

#align_import group_theory.perm.cycle.basic from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"

/-!
# Cyclic permutations

This file develops the theory of cycles in permutations.

## Main definitions

In the following, `f : Equiv.Perm β`.

* `Equiv.Perm.SameCycle`: `f.SameCycle x y` when `x` and `y` are in the same cycle of `f`.
* `Equiv.Perm.IsCycle`: `f` is a cycle if any two nonfixed points of `f` are related by repeated
  applications of `f`, and `f` is not the identity.
* `Equiv.Perm.IsCycleOn`: `f` is a cycle on a set `s` when any two points of `s` are related by
  repeated applications of `f`.

The following two definitions require that `β` is a `Fintype`:

* `Equiv.Perm.cycleOf`: `f.cycleOf x` is the cycle of `f` that `x` belongs to.
* `Equiv.Perm.cycleFactors`: `f.cycleFactors` is a list of disjoint cyclic permutations that
  multiply to `f`.

## Main results

* This file contains several closure results:
  - `closure_is_cycle` : The symmetric group is generated by cycles
  - `closure_cycle_adjacent_swap` : The symmetric group is generated by
    a cycle and an adjacent transposition
  - `closure_cycle_coprime_swap` : The symmetric group is generated by
    a cycle and a coprime transposition
  - `closure_prime_cycle_swap` : The symmetric group is generated by
    a prime cycle and a transposition

## Notes

`Equiv.Perm.is_cycle` and `Equiv.Perm.IsCycleOn` are different in three ways:
* `is_cycle` is about the entire type while `IsCycleOn` is restricted to a set.
* `is_cycle` forbids the identity while `IsCycleOn` allows it (if `s` is a subsingleton).
* `IsCycleOn` forbids fixed points on `s` (if `s` is nontrivial), while `is_cycle` allows them.
-/


open Equiv Function Finset

open BigOperators

variable {ι α β : Type*}

namespace Equiv.Perm

/-! ### `SameCycle` -/


section SameCycle

variable {f g : Perm α} {p : α → Prop} {x y z : α}

/-- The equivalence relation indicating that two points are in the same cycle of a permutation. -/
def SameCycle (f : Perm α) (x y : α) : Prop :=
  ∃ i : ℤ, (f ^ i) x = y
#align equiv.perm.same_cycle Equiv.Perm.SameCycle

@[refl]
theorem SameCycle.refl (f : Perm α) (x : α) : SameCycle f x x :=
  ⟨0, rfl⟩
#align equiv.perm.same_cycle.refl Equiv.Perm.SameCycle.refl

theorem SameCycle.rfl : SameCycle f x x :=
  SameCycle.refl _ _
#align equiv.perm.same_cycle.rfl Equiv.Perm.SameCycle.rfl

protected theorem _root_.Eq.sameCycle (h : x = y) (f : Perm α) : f.SameCycle x y := by rw [h]
#align eq.same_cycle Eq.sameCycle

@[symm]
theorem SameCycle.symm : SameCycle f x y → SameCycle f y x := fun ⟨i, hi⟩ =>
  ⟨-i, by rw [zpow_neg, ← hi, inv_apply_self]⟩
#align equiv.perm.same_cycle.symm Equiv.Perm.SameCycle.symm

theorem sameCycle_comm : SameCycle f x y ↔ SameCycle f y x :=
  ⟨SameCycle.symm, SameCycle.symm⟩
#align equiv.perm.same_cycle_comm Equiv.Perm.sameCycle_comm

@[trans]
theorem SameCycle.trans : SameCycle f x y → SameCycle f y z → SameCycle f x z :=
  fun ⟨i, hi⟩ ⟨j, hj⟩ => ⟨j + i, by rw [zpow_add, mul_apply, hi, hj]⟩
#align equiv.perm.same_cycle.trans Equiv.Perm.SameCycle.trans

variable (f) in
theorem SameCycle.equivalence : Equivalence (SameCycle f) :=
  ⟨SameCycle.refl f, SameCycle.symm, SameCycle.trans⟩

/-- The setoid defined by the `SameCycle` relation. -/
def SameCycle.setoid (f : Perm α) : Setoid α where
  iseqv := SameCycle.equivalence f

@[simp]
theorem sameCycle_one : SameCycle 1 x y ↔ x = y := by simp [SameCycle]
#align equiv.perm.same_cycle_one Equiv.Perm.sameCycle_one

@[simp]
theorem sameCycle_inv : SameCycle f⁻¹ x y ↔ SameCycle f x y :=
  (Equiv.neg _).exists_congr_left.trans <| by simp [SameCycle]
#align equiv.perm.same_cycle_inv Equiv.Perm.sameCycle_inv

alias ⟨SameCycle.of_inv, SameCycle.inv⟩ := sameCycle_inv
#align equiv.perm.same_cycle.of_inv Equiv.Perm.SameCycle.of_inv
#align equiv.perm.same_cycle.inv Equiv.Perm.SameCycle.inv

@[simp]
theorem sameCycle_conj : SameCycle (g * f * g⁻¹) x y ↔ SameCycle f (g⁻¹ x) (g⁻¹ y) :=
  exists_congr fun i => by simp [conj_zpow, eq_inv_iff_eq]
#align equiv.perm.same_cycle_conj Equiv.Perm.sameCycle_conj

theorem SameCycle.conj : SameCycle f x y → SameCycle (g * f * g⁻¹) (g x) (g y) := by
  simp [sameCycle_conj]
#align equiv.perm.same_cycle.conj Equiv.Perm.SameCycle.conj

theorem SameCycle.apply_eq_self_iff : SameCycle f x y → (f x = x ↔ f y = y) := fun ⟨i, hi⟩ => by
  rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
    (f ^ i).injective.eq_iff]
#align equiv.perm.same_cycle.apply_eq_self_iff Equiv.Perm.SameCycle.apply_eq_self_iff

theorem SameCycle.eq_of_left (h : SameCycle f x y) (hx : IsFixedPt f x) : x = y :=
  let ⟨_, hn⟩ := h
  (hx.perm_zpow _).eq.symm.trans hn
#align equiv.perm.same_cycle.eq_of_left Equiv.Perm.SameCycle.eq_of_left

theorem SameCycle.eq_of_right (h : SameCycle f x y) (hy : IsFixedPt f y) : x = y :=
  h.eq_of_left <| h.apply_eq_self_iff.2 hy
#align equiv.perm.same_cycle.eq_of_right Equiv.Perm.SameCycle.eq_of_right

@[simp]
theorem sameCycle_apply_left : SameCycle f (f x) y ↔ SameCycle f x y :=
  (Equiv.addRight 1).exists_congr_left.trans <| by
    simp [zpow_sub, SameCycle, Int.add_neg_one, Function.comp]
#align equiv.perm.same_cycle_apply_left Equiv.Perm.sameCycle_apply_left

@[simp]
theorem sameCycle_apply_right : SameCycle f x (f y) ↔ SameCycle f x y := by
  rw [sameCycle_comm, sameCycle_apply_left, sameCycle_comm]
#align equiv.perm.same_cycle_apply_right Equiv.Perm.sameCycle_apply_right

@[simp]
theorem sameCycle_inv_apply_left : SameCycle f (f⁻¹ x) y ↔ SameCycle f x y := by
  rw [← sameCycle_apply_left, apply_inv_self]
#align equiv.perm.same_cycle_inv_apply_left Equiv.Perm.sameCycle_inv_apply_left

@[simp]
theorem sameCycle_inv_apply_right : SameCycle f x (f⁻¹ y) ↔ SameCycle f x y := by
  rw [← sameCycle_apply_right, apply_inv_self]
#align equiv.perm.same_cycle_inv_apply_right Equiv.Perm.sameCycle_inv_apply_right

@[simp]
theorem sameCycle_zpow_left {n : ℤ} : SameCycle f ((f ^ n) x) y ↔ SameCycle f x y :=
  (Equiv.addRight (n : ℤ)).exists_congr_left.trans <| by simp [SameCycle, zpow_add]
#align equiv.perm.same_cycle_zpow_left Equiv.Perm.sameCycle_zpow_left

@[simp]
theorem sameCycle_zpow_right {n : ℤ} : SameCycle f x ((f ^ n) y) ↔ SameCycle f x y := by
  rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]
#align equiv.perm.same_cycle_zpow_right Equiv.Perm.sameCycle_zpow_right

@[simp]
theorem sameCycle_pow_left {n : ℕ} : SameCycle f ((f ^ n) x) y ↔ SameCycle f x y := by
  rw [← zpow_ofNat, sameCycle_zpow_left]
#align equiv.perm.same_cycle_pow_left Equiv.Perm.sameCycle_pow_left

@[simp]
theorem sameCycle_pow_right {n : ℕ} : SameCycle f x ((f ^ n) y) ↔ SameCycle f x y := by
  rw [← zpow_ofNat, sameCycle_zpow_right]
#align equiv.perm.same_cycle_pow_right Equiv.Perm.sameCycle_pow_right

alias ⟨SameCycle.of_apply_left, SameCycle.apply_left⟩ := sameCycle_apply_left
#align equiv.perm.same_cycle.of_apply_left Equiv.Perm.SameCycle.of_apply_left
#align equiv.perm.same_cycle.apply_left Equiv.Perm.SameCycle.apply_left

alias ⟨SameCycle.of_apply_right, SameCycle.apply_right⟩ := sameCycle_apply_right
#align equiv.perm.same_cycle.of_apply_right Equiv.Perm.SameCycle.of_apply_right
#align equiv.perm.same_cycle.apply_right Equiv.Perm.SameCycle.apply_right

alias ⟨SameCycle.of_inv_apply_left, SameCycle.inv_apply_left⟩ := sameCycle_inv_apply_left
#align equiv.perm.same_cycle.of_inv_apply_left Equiv.Perm.SameCycle.of_inv_apply_left
#align equiv.perm.same_cycle.inv_apply_left Equiv.Perm.SameCycle.inv_apply_left

alias ⟨SameCycle.of_inv_apply_right, SameCycle.inv_apply_right⟩ := sameCycle_inv_apply_right
#align equiv.perm.same_cycle.of_inv_apply_right Equiv.Perm.SameCycle.of_inv_apply_right
#align equiv.perm.same_cycle.inv_apply_right Equiv.Perm.SameCycle.inv_apply_right

alias ⟨SameCycle.of_pow_left, SameCycle.pow_left⟩ := sameCycle_pow_left
#align equiv.perm.same_cycle.of_pow_left Equiv.Perm.SameCycle.of_pow_left
#align equiv.perm.same_cycle.pow_left Equiv.Perm.SameCycle.pow_left

alias ⟨SameCycle.of_pow_right, SameCycle.pow_right⟩ := sameCycle_pow_right
#align equiv.perm.same_cycle.of_pow_right Equiv.Perm.SameCycle.of_pow_right
#align equiv.perm.same_cycle.pow_right Equiv.Perm.SameCycle.pow_right

alias ⟨SameCycle.of_zpow_left, SameCycle.zpow_left⟩ := sameCycle_zpow_left
#align equiv.perm.same_cycle.of_zpow_left Equiv.Perm.SameCycle.of_zpow_left
#align equiv.perm.same_cycle.zpow_left Equiv.Perm.SameCycle.zpow_left

alias ⟨SameCycle.of_zpow_right, SameCycle.zpow_right⟩ := sameCycle_zpow_right
#align equiv.perm.same_cycle.of_zpow_right Equiv.Perm.SameCycle.of_zpow_right
#align equiv.perm.same_cycle.zpow_right Equiv.Perm.SameCycle.zpow_right

theorem SameCycle.of_pow {n : ℕ} : SameCycle (f ^ n) x y → SameCycle f x y := fun ⟨m, h⟩ =>
  ⟨n * m, by simp [zpow_mul, h]⟩
#align equiv.perm.same_cycle.of_pow Equiv.Perm.SameCycle.of_pow

theorem SameCycle.of_zpow {n : ℤ} : SameCycle (f ^ n) x y → SameCycle f x y := fun ⟨m, h⟩ =>
  ⟨n * m, by simp [zpow_mul, h]⟩
#align equiv.perm.same_cycle.of_zpow Equiv.Perm.SameCycle.of_zpow

@[simp]
theorem sameCycle_subtypePerm {h} {x y : { x // p x }} :
    (f.subtypePerm h).SameCycle x y ↔ f.SameCycle x y :=
  exists_congr fun n => by simp [Subtype.ext_iff]
#align equiv.perm.same_cycle_subtype_perm Equiv.Perm.sameCycle_subtypePerm

alias ⟨_, SameCycle.subtypePerm⟩ := sameCycle_subtypePerm
#align equiv.perm.same_cycle.subtype_perm Equiv.Perm.SameCycle.subtypePerm

@[simp]
theorem sameCycle_extendDomain {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} :
    SameCycle (g.extendDomain f) (f x) (f y) ↔ g.SameCycle x y :=
  exists_congr fun n => by
    rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]
#align equiv.perm.same_cycle_extend_domain Equiv.Perm.sameCycle_extendDomain

alias ⟨_, SameCycle.extendDomain⟩ := sameCycle_extendDomain
#align equiv.perm.same_cycle.extend_domain Equiv.Perm.SameCycle.extendDomain

theorem SameCycle.exists_pow_eq' [Finite α] : SameCycle f x y → ∃ i < orderOf f, (f ^ i) x = y := by
  classical
    rintro ⟨k, rfl⟩
    use (k % orderOf f).natAbs
    have h₀ := Int.coe_nat_pos.mpr (orderOf_pos f)
    have h₁ := Int.emod_nonneg k h₀.ne'
    rw [← zpow_ofNat, Int.natAbs_of_nonneg h₁, ← zpow_eq_mod_orderOf]
    refine' ⟨_, by rfl⟩
    rw [← Int.ofNat_lt, Int.natAbs_of_nonneg h₁]
    exact Int.emod_lt_of_pos _ h₀
#align equiv.perm.same_cycle.exists_pow_eq' Equiv.Perm.SameCycle.exists_pow_eq'

theorem SameCycle.exists_pow_eq'' [Finite α] (h : SameCycle f x y) :
    ∃ (i : ℕ) (_ : 0 < i) (_ : i ≤ orderOf f), (f ^ i) x = y := by
  classical
    obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq'
    · refine' ⟨orderOf f, orderOf_pos f, le_rfl, _⟩
      rw [pow_orderOf_eq_one, pow_zero]
    · exact ⟨i.succ, i.zero_lt_succ, hi.le, by rfl⟩
#align equiv.perm.same_cycle.exists_pow_eq'' Equiv.Perm.SameCycle.exists_pow_eq''

instance [Fintype α] [DecidableEq α] (f : Perm α) : DecidableRel (SameCycle f) := fun x y =>
  decidable_of_iff (∃ n ∈ List.range (Fintype.card (Perm α)), (f ^ n) x = y)
    ⟨fun ⟨n, _, hn⟩ => ⟨n, hn⟩, fun ⟨i, hi⟩ => ⟨(i % orderOf f).natAbs,
      List.mem_range.2 (Int.ofNat_lt.1 <| by
        rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ <| Int.coe_nat_ne_zero.2 (orderOf_pos _).ne')]
        · refine' (Int.emod_lt _ <| Int.coe_nat_ne_zero_iff_pos.2 <| orderOf_pos _).trans_le _
          simp [orderOf_le_card_univ]),
      by
        rw [← zpow_ofNat, Int.natAbs_of_nonneg (Int.emod_nonneg _ <|
          Int.coe_nat_ne_zero_iff_pos.2 <| orderOf_pos _), ← zpow_eq_mod_orderOf, hi]⟩⟩

end SameCycle

/-!
### `IsCycle`
-/


section IsCycle

variable {f g : Perm α} {x y : α}

/-- A cycle is a non identity permutation where any two nonfixed points of the permutation are
related by repeated application of the permutation. -/
def IsCycle (f : Perm α) : Prop :=
  ∃ x, f x ≠ x ∧ ∀ ⦃y⦄, f y ≠ y → SameCycle f x y
#align equiv.perm.is_cycle Equiv.Perm.IsCycle

theorem IsCycle.ne_one (h : IsCycle f) : f ≠ 1 := fun hf => by simp [hf, IsCycle] at h
#align equiv.perm.is_cycle.ne_one Equiv.Perm.IsCycle.ne_one

@[simp]
theorem not_isCycle_one : ¬(1 : Perm α).IsCycle := fun H => H.ne_one rfl
#align equiv.perm.not_is_cycle_one Equiv.Perm.not_isCycle_one

protected theorem IsCycle.sameCycle (hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) :
    SameCycle f x y :=
  let ⟨g, hg⟩ := hf
  let ⟨a, ha⟩ := hg.2 hx
  let ⟨b, hb⟩ := hg.2 hy
  ⟨b - a, by rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]⟩
#align equiv.perm.is_cycle.same_cycle Equiv.Perm.IsCycle.sameCycle

theorem IsCycle.exists_zpow_eq : IsCycle f → f x ≠ x → f y ≠ y → ∃ i : ℤ, (f ^ i) x = y :=
  IsCycle.sameCycle
#align equiv.perm.is_cycle.exists_zpow_eq Equiv.Perm.IsCycle.exists_zpow_eq

theorem IsCycle.inv (hf : IsCycle f) : IsCycle f⁻¹ :=
  hf.imp fun _ ⟨hx, h⟩ =>
    ⟨inv_eq_iff_eq.not.2 hx.symm, fun _ hy => (h <| inv_eq_iff_eq.not.2 hy.symm).inv⟩
#align equiv.perm.is_cycle.inv Equiv.Perm.IsCycle.inv

@[simp]
theorem isCycle_inv : IsCycle f⁻¹ ↔ IsCycle f :=
  ⟨fun h => h.inv, IsCycle.inv⟩
#align equiv.perm.is_cycle_inv Equiv.Perm.isCycle_inv

theorem IsCycle.conj : IsCycle f → IsCycle (g * f * g⁻¹) := by
  rintro ⟨x, hx, h⟩
  refine' ⟨g x, by simp [coe_mul, inv_apply_self, hx], fun y hy => _⟩
  rw [← apply_inv_self g y]
  exact (h <| eq_inv_iff_eq.not.2 hy).conj
#align equiv.perm.is_cycle.conj Equiv.Perm.IsCycle.conj

protected theorem IsCycle.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
    IsCycle g → IsCycle (g.extendDomain f) := by
  rintro ⟨a, ha, ha'⟩
  refine' ⟨f a, _, fun b hb => _⟩
  · rw [extendDomain_apply_image]
    exact Subtype.coe_injective.ne (f.injective.ne ha)
  have h : b = f (f.symm ⟨b, of_not_not <| hb ∘ extendDomain_apply_not_subtype _ _⟩) := by
    rw [apply_symm_apply, Subtype.coe_mk]
  rw [h] at hb ⊢
  simp only [extendDomain_apply_image, Subtype.coe_injective.ne_iff, f.injective.ne_iff] at hb
  exact (ha' hb).extendDomain
#align equiv.perm.is_cycle.extend_domain Equiv.Perm.IsCycle.extendDomain

theorem isCycle_iff_sameCycle (hx : f x ≠ x) : IsCycle f ↔ ∀ {y}, SameCycle f x y ↔ f y ≠ y :=
  ⟨fun hf y =>
    ⟨fun ⟨i, hi⟩ hy =>
      hx <| by
        rw [← zpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi
        rw [hi, hy],
      hf.exists_zpow_eq hx⟩,
    fun h => ⟨x, hx, fun y hy => h.2 hy⟩⟩
#align equiv.perm.is_cycle_iff_same_cycle Equiv.Perm.isCycle_iff_sameCycle

section Finite

variable [Finite α]

theorem IsCycle.exists_pow_eq (hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) :
    ∃ i : ℕ, (f ^ i) x = y := by
  let ⟨n, hn⟩ := hf.exists_zpow_eq hx hy
  classical exact
      ⟨(n % orderOf f).toNat, by
        {have := n.emod_nonneg (Int.coe_nat_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
         rwa [← zpow_ofNat, Int.toNat_of_nonneg this, ← zpow_eq_mod_orderOf]}⟩
#align equiv.perm.is_cycle.exists_pow_eq Equiv.Perm.IsCycle.exists_pow_eq

end Finite

variable [DecidableEq α]

theorem isCycle_swap (hxy : x ≠ y) : IsCycle (swap x y) :=
  ⟨y, by rwa [swap_apply_right], fun a (ha : ite (a = x) y (ite (a = y) x a) ≠ a) =>
    if hya : y = a then ⟨0, hya⟩
    else
      ⟨1, by
        rw [zpow_one, swap_apply_def]
        split_ifs at * <;> tauto⟩⟩
#align equiv.perm.is_cycle_swap Equiv.Perm.isCycle_swap

protected theorem IsSwap.isCycle : IsSwap f → IsCycle f := by
  rintro ⟨x, y, hxy, rfl⟩
  exact isCycle_swap hxy
#align equiv.perm.is_swap.is_cycle Equiv.Perm.IsSwap.isCycle

variable [Fintype α]

theorem IsCycle.two_le_card_support (h : IsCycle f) : 2 ≤ f.support.card :=
  two_le_card_support_of_ne_one h.ne_one
#align equiv.perm.is_cycle.two_le_card_support Equiv.Perm.IsCycle.two_le_card_support

theorem IsCycle.exists_pow_eq_one [Finite β] {f : Perm β} (hf : IsCycle f) :
    ∃ (k : ℕ) (_ : 1 < k), f ^ k = 1 := by
  classical
    have : IsOfFinOrder f := by exact _root_.exists_pow_eq_one f
    rw [isOfFinOrder_iff_pow_eq_one] at this
    obtain ⟨x, hx, _⟩ := hf
    obtain ⟨_ | _ | k, hk, hk'⟩ := this
    · exact absurd hk (lt_asymm hk)
    · rw [pow_one] at hk'
      simp [hk'] at hx
    · exact ⟨k + 2, by simp, hk'⟩
#align equiv.perm.is_cycle.exists_pow_eq_one Equiv.Perm.IsCycle.exists_pow_eq_one

/-- The subgroup generated by a cycle is in bijection with its support -/
noncomputable def IsCycle.zpowersEquivSupport {σ : Perm α} (hσ : IsCycle σ) :
    (Subgroup.zpowers σ) ≃ σ.support :=
  Equiv.ofBijective
    (fun (τ : ↥ ((Subgroup.zpowers σ) : Set (Perm α))) =>
      ⟨(τ : Perm α) (Classical.choose hσ), by
        obtain ⟨τ, n, rfl⟩ := τ
        erw [Finset.mem_coe, Subtype.coe_mk, zpow_apply_mem_support, mem_support]
        exact (Classical.choose_spec hσ).1⟩)
    (by
      constructor
      · rintro ⟨a, m, rfl⟩ ⟨b, n, rfl⟩ h
        ext y
        by_cases hy : σ y = y
        · simp_rw [zpow_apply_eq_self_of_apply_eq_self hy]
        · obtain ⟨i, rfl⟩ := (Classical.choose_spec hσ).2 hy
          rw [Subtype.coe_mk, Subtype.coe_mk, zpow_apply_comm σ m i, zpow_apply_comm σ n i]
          exact congr_arg _ (Subtype.ext_iff.mp h)
      · rintro ⟨y, hy⟩
        erw [Finset.mem_coe, mem_support] at hy
        obtain ⟨n, rfl⟩ := (Classical.choose_spec hσ).2 hy
        exact ⟨⟨σ ^ n, n, rfl⟩, rfl⟩)
#align equiv.perm.is_cycle.zpowers_equiv_support Equiv.Perm.IsCycle.zpowersEquivSupport

@[simp]
theorem IsCycle.zpowersEquivSupport_apply {σ : Perm α} (hσ : IsCycle σ) {n : ℕ} :
    hσ.zpowersEquivSupport ⟨σ ^ n, n, rfl⟩ =
      ⟨(σ ^ n) (Classical.choose hσ),
        pow_apply_mem_support.2 (mem_support.2 (Classical.choose_spec hσ).1)⟩ :=
  rfl
#align equiv.perm.is_cycle.zpowers_equiv_support_apply Equiv.Perm.IsCycle.zpowersEquivSupport_apply

@[simp]
theorem IsCycle.zpowersEquivSupport_symm_apply {σ : Perm α} (hσ : IsCycle σ) (n : ℕ) :
    hσ.zpowersEquivSupport.symm
        ⟨(σ ^ n) (Classical.choose hσ),
          pow_apply_mem_support.2 (mem_support.2 (Classical.choose_spec hσ).1)⟩ =
      ⟨σ ^ n, n, rfl⟩ :=
  (Equiv.symm_apply_eq _).2 hσ.zpowersEquivSupport_apply
#align equiv.perm.is_cycle.zpowers_equiv_support_symm_apply Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply

protected theorem IsCycle.orderOf (hf : IsCycle f) : orderOf f = f.support.card := by
  rw [orderOf_eq_card_zpowers, ← Fintype.card_coe]
  convert Fintype.card_congr (IsCycle.zpowersEquivSupport hf)
#align equiv.perm.is_cycle.order_of Equiv.Perm.IsCycle.orderOf

theorem isCycle_swap_mul_aux₁ {α : Type*} [DecidableEq α] :
    ∀ (n : ℕ) {b x : α} {f : Perm α} (_ : (swap x (f x) * f) b ≠ b) (_ : (f ^ n) (f x) = b),
      ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b := by
  intro n
  induction' n with n hn
  · exact fun _ h => ⟨0, h⟩
  · intro b x f hb h
    exact if hfbx : f x = b then ⟨0, hfbx⟩
      else
        have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
        have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b := by
          rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx), Ne.def, ←
            f.injective.eq_iff, apply_inv_self]
          exact this.1
        let ⟨i, hi⟩ := hn hb' (f.injective <| by
          rw [apply_inv_self]; rwa [pow_succ, mul_apply] at h)
        ⟨i + 1, by
          rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_inv_self,
            swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (Ne.symm hfbx)]⟩
#align equiv.perm.is_cycle_swap_mul_aux₁ Equiv.Perm.isCycle_swap_mul_aux₁

theorem isCycle_swap_mul_aux₂ {α : Type*} [DecidableEq α] :
    ∀ (n : ℤ) {b x : α} {f : Perm α} (_ : (swap x (f x) * f) b ≠ b) (_ : (f ^ n) (f x) = b),
      ∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b := by
  intro n
  induction' n with n n
  · exact isCycle_swap_mul_aux₁ n
  · intro b x f hb h
    exact if hfbx' : f x = b then ⟨0, hfbx'⟩
      else
        have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
        have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b := by
          rw [mul_apply, swap_apply_def]
          split_ifs <;>
              simp only [inv_eq_iff_eq, Perm.mul_apply, zpow_negSucc,
                Ne.def, Perm.apply_inv_self] at
                * <;> tauto
        let ⟨i, hi⟩ :=
          isCycle_swap_mul_aux₁ n hb
            (show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b by
              rw [← zpow_ofNat, ← h, ← mul_apply, ← mul_apply, ← mul_apply, zpow_negSucc, ← inv_pow,
                pow_succ', mul_assoc, mul_assoc, inv_mul_self, mul_one, zpow_ofNat, ← pow_succ', ←
                pow_succ])
        have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x := by
          rw [mul_apply, inv_apply_self, swap_apply_left]
        ⟨-i, by
          rw [← add_sub_cancel i 1, neg_sub, sub_eq_add_neg, zpow_add, zpow_one, zpow_neg,
            ← inv_zpow, mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x,
            zpow_add, zpow_one, mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self,
            swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx')]⟩
#align equiv.perm.is_cycle_swap_mul_aux₂ Equiv.Perm.isCycle_swap_mul_aux₂

theorem IsCycle.eq_swap_of_apply_apply_eq_self {α : Type*} [DecidableEq α] {f : Perm α}
    (hf : IsCycle f) {x : α} (hfx : f x ≠ x) (hffx : f (f x) = x) : f = swap x (f x) :=
  Equiv.ext fun y =>
    let ⟨z, hz⟩ := hf
    let ⟨i, hi⟩ := hz.2 hfx
    if hyx : y = x then by simp [hyx]
    else
      if hfyx : y = f x then by simp [hfyx, hffx]
      else by
        rw [swap_apply_of_ne_of_ne hyx hfyx]
        refine' by_contradiction fun hy => _
        cases' hz.2 hy with j hj
        rw [← sub_add_cancel j i, zpow_add, mul_apply, hi] at hj
        cases' zpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji hji
        · rw [← hj, hji] at hyx
          tauto
        · rw [← hj, hji] at hfyx
          tauto
#align equiv.perm.is_cycle.eq_swap_of_apply_apply_eq_self Equiv.Perm.IsCycle.eq_swap_of_apply_apply_eq_self

theorem IsCycle.swap_mul {α : Type*} [DecidableEq α] {f : Perm α} (hf : IsCycle f) {x : α}
    (hx : f x ≠ x) (hffx : f (f x) ≠ x) : IsCycle (swap x (f x) * f) :=
  ⟨f x, by simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, if_neg hx, hx],
    fun y hy =>
    let ⟨i, hi⟩ := hf.exists_zpow_eq hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1
    -- Porting note: Needed to add Perm α typehint, otherwise does not know how to coerce to fun
    have hi : (f ^ (i - 1) : Perm α) (f x) = y :=
      calc
        (f ^ (i - 1) : Perm α) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ) : Perm α) x := by simp
        _ = y := by rwa [← zpow_add, sub_add_cancel]

    isCycle_swap_mul_aux₂ (i - 1) hy hi⟩
#align equiv.perm.is_cycle.swap_mul Equiv.Perm.IsCycle.swap_mul

theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ f.support.card :=
  let ⟨x, hx⟩ := hf
  calc
    Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f)) := by
      {rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]}
    _ = -(-1) ^ f.support.card :=
      if h1 : f (f x) = x then by
        have h : swap x (f x) * f = 1 := by
          simp only [mul_def, one_def]
          rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
        dsimp only
        rw [sign_mul, sign_swap hx.1.symm, h, sign_one,
          hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm]
        rfl
      else by
        have h : card (support (swap x (f x) * f)) + 1 = card (support f) := by
          rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase]
        have : card (support (swap x (f x) * f)) < card (support f) :=
          card_support_swap_mul hx.1
        dsimp only
        rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]
        simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one]
termination_by _ => f.support.card
#align equiv.perm.is_cycle.sign Equiv.Perm.IsCycle.sign

theorem IsCycle.of_pow {n : ℕ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) :
    IsCycle f := by
  have key : ∀ x : α, (f ^ n) x ≠ x ↔ f x ≠ x := by
    simp_rw [← mem_support, ← Finset.ext_iff]
    exact (support_pow_le _ n).antisymm h2
  obtain ⟨x, hx1, hx2⟩ := h1
  refine' ⟨x, (key x).mp hx1, fun y hy => _⟩
  cases' hx2 ((key y).mpr hy) with i _
  exact ⟨n * i, by rwa [zpow_mul]⟩
#align equiv.perm.is_cycle.of_pow Equiv.Perm.IsCycle.of_pow

-- The lemma `support_zpow_le` is relevant. It means that `h2` is equivalent to
-- `σ.support = (σ ^ n).support`, as well as to `σ.support.card ≤ (σ ^ n).support.card`.
theorem IsCycle.of_zpow {n : ℤ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) :
    IsCycle f := by
  cases n
  · exact h1.of_pow h2
  · simp only [le_eq_subset, zpow_negSucc, Perm.support_inv] at h1 h2
    exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2
#align equiv.perm.is_cycle.of_zpow Equiv.Perm.IsCycle.of_zpow

theorem nodup_of_pairwise_disjoint_cycles {l : List (Perm β)} (h1 : ∀ f ∈ l, IsCycle f)
    (h2 : l.Pairwise Disjoint) : l.Nodup :=
  nodup_of_pairwise_disjoint (fun h => (h1 1 h).ne_one rfl) h2
#align equiv.perm.nodup_of_pairwise_disjoint_cycles Equiv.Perm.nodup_of_pairwise_disjoint_cycles

/-- Unlike `support_congr`, which assumes that `∀ (x ∈ g.support), f x = g x)`, here
we have the weaker assumption that `∀ (x ∈ f.support), f x = g x`. -/
theorem IsCycle.support_congr (hf : IsCycle f) (hg : IsCycle g) (h : f.support ⊆ g.support)
    (h' : ∀ x ∈ f.support, f x = g x) : f = g := by
  have : f.support = g.support := by
    refine' le_antisymm h _
    intro z hz
    obtain ⟨x, hx, _⟩ := id hf
    have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
    obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)
    have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x := by
      intro x hx
      exact h' x (mem_of_mem_inter_left hx)
    rwa [← hm, ←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
      pow_apply_mem_support, mem_support]
  refine' Equiv.Perm.support_congr h _
  simpa [← this] using h'
#align equiv.perm.is_cycle.support_congr Equiv.Perm.IsCycle.support_congr

/-- If two cyclic permutations agree on all terms in their intersection,
and that intersection is not empty, then the two cyclic permutations must be equal. -/
theorem IsCycle.eq_on_support_inter_nonempty_congr (hf : IsCycle f) (hg : IsCycle g)
    (h : ∀ x ∈ f.support ∩ g.support, f x = g x)
    (hx : f x = g x) (hx' : x ∈ f.support) : f = g := by
  have hx'' : x ∈ g.support := by rwa [mem_support, ← hx, ← mem_support]
  have : f.support ⊆ g.support := by
    intro y hy
    obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)
    rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]
  rw [(inter_eq_left_iff_subset _ _).mpr this] at h
  exact hf.support_congr hg this h
#align equiv.perm.is_cycle.eq_on_support_inter_nonempty_congr Equiv.Perm.IsCycle.eq_on_support_inter_nonempty_congr

theorem IsCycle.support_pow_eq_iff (hf : IsCycle f) {n : ℕ} :
    support (f ^ n) = support f ↔ ¬orderOf f ∣ n := by
  rw [orderOf_dvd_iff_pow_eq_one]
  constructor
  · intro h H
    refine' hf.ne_one _
    rw [← support_eq_empty_iff, ← h, H, support_one]
  · intro H
    apply le_antisymm (support_pow_le _ n) _
    intro x hx
    contrapose! H
    ext z
    by_cases hz : f z = z
    · rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]
    · obtain ⟨k, rfl⟩ := hf.exists_pow_eq hz (mem_support.mp hx)
      apply (f ^ k).injective
      rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply]
      simpa using H
#align equiv.perm.is_cycle.support_pow_eq_iff Equiv.Perm.IsCycle.support_pow_eq_iff

theorem IsCycle.support_pow_of_pos_of_lt_orderOf (hf : IsCycle f) {n : ℕ} (npos : 0 < n)
    (hn : n < orderOf f) : (f ^ n).support = f.support :=
  hf.support_pow_eq_iff.2 <| Nat.not_dvd_of_pos_of_lt npos hn
#align equiv.perm.is_cycle.support_pow_of_pos_of_lt_order_of Equiv.Perm.IsCycle.support_pow_of_pos_of_lt_orderOf

theorem IsCycle.pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} :
    IsCycle (f ^ n) ↔ n.Coprime (orderOf f) := by
  classical
    cases nonempty_fintype β
    constructor
    · intro h
      have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine' h.ne_one _
        simp [pow_mul, pow_orderOf_eq_one]
      have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
      rw [orderOf_pow, Nat.div_eq_self] at this
      cases' this with h
      · exact absurd h (orderOf_pos _).ne'
      · rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
    · intro h
      obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
      have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
      refine' hf'.of_pow fun x hx => _
      rw [hm]
      exact support_pow_le _ n hx
#align equiv.perm.is_cycle.pow_iff Equiv.Perm.IsCycle.pow_iff

-- TODO: Define a `Set`-valued support to get rid of the `Finite β` assumption
theorem IsCycle.pow_eq_one_iff [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} :
    f ^ n = 1 ↔ ∃ x, f x ≠ x ∧ (f ^ n) x = x := by
  classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      by_cases h : support (f ^ n) = support f
      · rw [← mem_support, ← h, mem_support] at hx
        contradiction
      · rw [hf.support_pow_eq_iff, Classical.not_not] at h
        obtain ⟨k, rfl⟩ := h
        rw [pow_mul, pow_orderOf_eq_one, one_pow]
#align equiv.perm.is_cycle.pow_eq_one_iff Equiv.Perm.IsCycle.pow_eq_one_iff

-- TODO: Define a `Set`-valued support to get rid of the `Finite β` assumption
theorem IsCycle.pow_eq_one_iff' [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} {x : β}
    (hx : f x ≠ x) : f ^ n = 1 ↔ (f ^ n) x = x :=
  ⟨fun h => FunLike.congr_fun h x, fun h => hf.pow_eq_one_iff.2 ⟨x, hx, h⟩⟩
#align equiv.perm.is_cycle.pow_eq_one_iff' Equiv.Perm.IsCycle.pow_eq_one_iff'

-- TODO: Define a `Set`-valued support to get rid of the `Finite β` assumption
theorem IsCycle.pow_eq_one_iff'' [Finite β] {f : Perm β} (hf : IsCycle f) {n : ℕ} :
    f ^ n = 1 ↔ ∀ x, f x ≠ x → (f ^ n) x = x :=
  ⟨fun h _ hx => (hf.pow_eq_one_iff' hx).1 h, fun h =>
    let ⟨_, hx, _⟩ := id hf
    (hf.pow_eq_one_iff' hx).2 (h _ hx)⟩
#align equiv.perm.is_cycle.pow_eq_one_iff'' Equiv.Perm.IsCycle.pow_eq_one_iff''

-- TODO: Define a `Set`-valued support to get rid of the `Finite β` assumption
theorem IsCycle.pow_eq_pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {a b : ℕ} :
    f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x := by
  classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      wlog hab : a ≤ b generalizing a b
      · exact (this hx'.symm (le_of_not_le hab)).symm
      suffices f ^ (b - a) = 1 by
        rw [pow_sub _ hab, mul_inv_eq_one] at this
        rw [this]
      rw [hf.pow_eq_one_iff]
      by_cases hfa : (f ^ a) x ∈ f.support
      · refine' ⟨(f ^ a) x, mem_support.mp hfa, _⟩
        simp only [pow_sub _ hab, Equiv.Perm.coe_mul, Function.comp_apply, inv_apply_self, ← hx']
      · have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x
        simp only [zpow_one, zpow_ofNat] at h
        rw [not_mem_support, h, Function.Injective.eq_iff (f ^ a).injective] at hfa
        contradiction
#align equiv.perm.is_cycle.pow_eq_pow_iff Equiv.Perm.IsCycle.pow_eq_pow_iff

theorem IsCycle.isCycle_pow_pos_of_lt_prime_order [Finite β] {f : Perm β} (hf : IsCycle f)
    (hf' : (orderOf f).Prime) (n : ℕ) (hn : 0 < n) (hn' : n < orderOf f) : IsCycle (f ^ n) := by
  classical
    cases nonempty_fintype β
    have : n.Coprime (orderOf f) := by
      refine' Nat.Coprime.symm _
      rw [Nat.Prime.coprime_iff_not_dvd hf']
      exact Nat.not_dvd_of_pos_of_lt hn hn'
    obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime this
    have hf'' := hf
    rw [← hm] at hf''
    refine' hf''.of_pow _
    rw [hm]
    exact support_pow_le f n
#align equiv.perm.is_cycle.is_cycle_pow_pos_of_lt_prime_order Equiv.Perm.IsCycle.isCycle_pow_pos_of_lt_prime_order

end IsCycle

/-! ### `IsCycleOn` -/


section IsCycleOn

variable {f g : Perm α} {s t : Set α} {a b x y : α}

/-- A permutation is a cycle on `s` when any two points of `s` are related by repeated application
of the permutation. Note that this means the identity is a cycle of subsingleton sets. -/
def IsCycleOn (f : Perm α) (s : Set α) : Prop :=
  Set.BijOn f s s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → f.SameCycle x y
#align equiv.perm.is_cycle_on Equiv.Perm.IsCycleOn

@[simp]
theorem isCycleOn_empty : f.IsCycleOn ∅ := by simp [IsCycleOn, Set.bijOn_empty]
#align equiv.perm.is_cycle_on_empty Equiv.Perm.isCycleOn_empty

@[simp]
theorem isCycleOn_one : (1 : Perm α).IsCycleOn s ↔ s.Subsingleton := by
  simp [IsCycleOn, Set.bijOn_id, Set.Subsingleton]
#align equiv.perm.is_cycle_on_one Equiv.Perm.isCycleOn_one

alias ⟨IsCycleOn.subsingleton, _root_.Set.Subsingleton.isCycleOn_one⟩ := isCycleOn_one
#align equiv.perm.is_cycle_on.subsingleton Equiv.Perm.IsCycleOn.subsingleton
#align set.subsingleton.is_cycle_on_one Set.Subsingleton.isCycleOn_one

@[simp]
theorem isCycleOn_singleton : f.IsCycleOn {a} ↔ f a = a := by simp [IsCycleOn, SameCycle.rfl]
#align equiv.perm.is_cycle_on_singleton Equiv.Perm.isCycleOn_singleton

theorem isCycleOn_of_subsingleton [Subsingleton α] (f : Perm α) (s : Set α) : f.IsCycleOn s :=
  ⟨s.bijOn_of_subsingleton _, fun x _ y _ => (Subsingleton.elim x y).sameCycle _⟩
#align equiv.perm.is_cycle_on_of_subsingleton Equiv.Perm.isCycleOn_of_subsingleton

@[simp]
theorem isCycleOn_inv : f⁻¹.IsCycleOn s ↔ f.IsCycleOn s := by
  simp only [IsCycleOn, sameCycle_inv, and_congr_left_iff]
  exact fun _ ↦ ⟨fun h ↦ Set.BijOn.perm_inv h, fun h ↦ Set.BijOn.perm_inv h⟩
#align equiv.perm.is_cycle_on_inv Equiv.Perm.isCycleOn_inv

alias ⟨IsCycleOn.of_inv, IsCycleOn.inv⟩ := isCycleOn_inv
#align equiv.perm.is_cycle_on.of_inv Equiv.Perm.IsCycleOn.of_inv
#align equiv.perm.is_cycle_on.inv Equiv.Perm.IsCycleOn.inv

theorem IsCycleOn.conj (h : f.IsCycleOn s) : (g * f * g⁻¹).IsCycleOn ((g : Perm α) '' s) :=
  ⟨(g.bijOn_image.comp h.1).comp g.bijOn_symm_image, fun x hx y hy => by
    rw [← preimage_inv] at hx hy
    convert Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g) <;> rw [apply_inv_self]⟩
#align equiv.perm.is_cycle_on.conj Equiv.Perm.IsCycleOn.conj

theorem isCycleOn_swap [DecidableEq α] (hab : a ≠ b) : (swap a b).IsCycleOn {a, b} :=
  ⟨bijOn_swap (by simp) (by simp), fun x hx y hy => by
    rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hx hy
    obtain rfl | rfl := hx <;> obtain rfl | rfl := hy
    · exact ⟨0, by rw [zpow_zero, coe_one, id.def]⟩
    · exact ⟨1, by rw [zpow_one, swap_apply_left]⟩
    · exact ⟨1, by rw [zpow_one, swap_apply_right]⟩
    · exact ⟨0, by rw [zpow_zero, coe_one, id.def]⟩⟩
#align equiv.perm.is_cycle_on_swap Equiv.Perm.isCycleOn_swap

protected theorem IsCycleOn.apply_ne (hf : f.IsCycleOn s) (hs : s.Nontrivial) (ha : a ∈ s) :
    f a ≠ a := by
  obtain ⟨b, hb, hba⟩ := hs.exists_ne a
  obtain ⟨n, rfl⟩ := hf.2 ha hb
  exact fun h => hba (IsFixedPt.perm_zpow h n)
#align equiv.perm.is_cycle_on.apply_ne Equiv.Perm.IsCycleOn.apply_ne

protected theorem IsCycle.isCycleOn (hf : f.IsCycle) : f.IsCycleOn { x | f x ≠ x } :=
  ⟨f.bijOn fun _ => f.apply_eq_iff_eq.not, fun _ ha _ => hf.sameCycle ha⟩
#align equiv.perm.is_cycle.is_cycle_on Equiv.Perm.IsCycle.isCycleOn

/-- This lemma demonstrates the relation between `Equiv.Perm.IsCycle` and `Equiv.Perm.IsCycleOn`
in non-degenerate cases. -/
theorem isCycle_iff_exists_isCycleOn :
    f.IsCycle ↔ ∃ s : Set α, s.Nontrivial ∧ f.IsCycleOn s ∧ ∀ ⦃x⦄, ¬IsFixedPt f x → x ∈ s := by
  refine' ⟨fun hf => ⟨{ x | f x ≠ x }, _, hf.isCycleOn, fun _ => id⟩, _⟩
  · obtain ⟨a, ha⟩ := hf
    exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩
  · rintro ⟨s, hs, hf, hsf⟩
    obtain ⟨a, ha⟩ := hs.nonempty
    exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩
#align equiv.perm.is_cycle_iff_exists_is_cycle_on Equiv.Perm.isCycle_iff_exists_isCycleOn

theorem IsCycleOn.apply_mem_iff (hf : f.IsCycleOn s) : f x ∈ s ↔ x ∈ s :=
  ⟨fun hx => by
    convert hf.1.perm_inv.1 hx
    rw [inv_apply_self], fun hx => hf.1.mapsTo hx⟩
#align equiv.perm.is_cycle_on.apply_mem_iff Equiv.Perm.IsCycleOn.apply_mem_iff

/-- Note that the identity satisfies `IsCycleOn` for any subsingleton set, but not `IsCycle`. -/
theorem IsCycleOn.isCycle_subtypePerm (hf : f.IsCycleOn s) (hs : s.Nontrivial) :
    (f.subtypePerm fun _ => hf.apply_mem_iff.symm : Perm s).IsCycle := by
  obtain ⟨a, ha⟩ := hs.nonempty
  exact
    ⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ =>
      (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩
#align equiv.perm.is_cycle_on.is_cycle_subtype_perm Equiv.Perm.IsCycleOn.isCycle_subtypePerm

/-- Note that the identity is a cycle on any subsingleton set, but not a cycle. -/
protected theorem IsCycleOn.subtypePerm (hf : f.IsCycleOn s) :
    (f.subtypePerm fun _ => hf.apply_mem_iff.symm : Perm s).IsCycleOn _root_.Set.univ := by
  obtain hs | hs := s.subsingleton_or_nontrivial
  · haveI := hs.coe_sort
    exact isCycleOn_of_subsingleton _ _
  convert (hf.isCycle_subtypePerm hs).isCycleOn
  rw [eq_comm, Set.eq_univ_iff_forall]
  exact fun x => ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs x.2)
#align equiv.perm.is_cycle_on.subtype_perm Equiv.Perm.IsCycleOn.subtypePerm

-- TODO: Theory of order of an element under an action
theorem IsCycleOn.pow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) {n : ℕ} :
    (f ^ n) a = a ↔ s.card ∣ n := by
  obtain rfl | hs := Finset.eq_singleton_or_nontrivial ha
  · rw [coe_singleton, isCycleOn_singleton] at hf
    simpa using IsFixedPt.iterate hf n
  classical
    have h : ∀ x ∈ s.attach, ¬f ↑x = ↑x := fun x _ => hf.apply_ne hs x.2
    have := (hf.isCycle_subtypePerm hs).orderOf
    simp only [coe_sort_coe, support_subtype_perm, ne_eq, decide_not, Bool.not_eq_true',
      decide_eq_false_iff_not, mem_attach, forall_true_left, Subtype.forall, filter_true_of_mem h,
      card_attach] at this
    rw [← this, orderOf_dvd_iff_pow_eq_one,
      (hf.isCycle_subtypePerm hs).pow_eq_one_iff'
        (ne_of_apply_ne ((↑) : s → α) <| hf.apply_ne hs (⟨a, ha⟩ : s).2)]
    simp
#align equiv.perm.is_cycle_on.pow_apply_eq Equiv.Perm.IsCycleOn.pow_apply_eq

theorem IsCycleOn.zpow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) :
    ∀ {n : ℤ}, (f ^ n) a = a ↔ (s.card : ℤ) ∣ n
  | Int.ofNat n => (hf.pow_apply_eq ha).trans Int.coe_nat_dvd.symm
  | Int.negSucc n => by
    rw [zpow_negSucc, ← inv_pow]
    exact (hf.inv.pow_apply_eq ha).trans (dvd_neg.trans Int.coe_nat_dvd).symm
#align equiv.perm.is_cycle_on.zpow_apply_eq Equiv.Perm.IsCycleOn.zpow_apply_eq

theorem IsCycleOn.pow_apply_eq_pow_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s)
    {m n : ℕ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD s.card] := by
  rw [Nat.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
  simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm]
#align equiv.perm.is_cycle_on.pow_apply_eq_pow_apply Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply

theorem IsCycleOn.zpow_apply_eq_zpow_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s)
    {m n : ℤ} : (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD s.card] := by
  rw [Int.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
  simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm]
#align equiv.perm.is_cycle_on.zpow_apply_eq_zpow_apply Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply

theorem IsCycleOn.pow_card_apply {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) :
    (f ^ s.card) a = a :=
  (hf.pow_apply_eq ha).2 dvd_rfl
#align equiv.perm.is_cycle_on.pow_card_apply Equiv.Perm.IsCycleOn.pow_card_apply

theorem IsCycleOn.exists_pow_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) :
    ∃ n < s.card, (f ^ n) a = b := by
  classical
    obtain ⟨n, rfl⟩ := hf.2 ha hb
    obtain ⟨k, hk⟩ := (Int.mod_modEq n s.card).symm.dvd
    refine' ⟨n.natMod s.card, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', _⟩
    rw [← zpow_ofNat, Int.natMod,
      Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
        (Nonempty.card_pos ⟨a, ha⟩).ne'), sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
    simp only [zpow_coe_nat, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]
    exact IsFixedPt.perm_zpow (hf.pow_card_apply ha) _
#align equiv.perm.is_cycle_on.exists_pow_eq Equiv.Perm.IsCycleOn.exists_pow_eq

theorem IsCycleOn.exists_pow_eq' (hs : s.Finite) (hf : f.IsCycleOn s) (ha : a ∈ s) (hb : b ∈ s) :
    ∃ n : ℕ, (f ^ n) a = b := by
  lift s to Finset α using id hs
  obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb
  exact ⟨n, hn⟩
#align equiv.perm.is_cycle_on.exists_pow_eq' Equiv.Perm.IsCycleOn.exists_pow_eq'

theorem IsCycleOn.range_pow (hs : s.Finite) (h : f.IsCycleOn s) (ha : a ∈ s) :
    Set.range (fun n => (f ^ n) a : ℕ → α) = s :=
  Set.Subset.antisymm (Set.range_subset_iff.2 fun _ => h.1.mapsTo.perm_pow _ ha) fun _ =>
    h.exists_pow_eq' hs ha
#align equiv.perm.is_cycle_on.range_pow Equiv.Perm.IsCycleOn.range_pow

theorem IsCycleOn.range_zpow (h : f.IsCycleOn s) (ha : a ∈ s) :
    Set.range (fun n => (f ^ n) a : ℤ → α) = s :=
  Set.Subset.antisymm (Set.range_subset_iff.2 fun _ => (h.1.perm_zpow _).mapsTo ha) <| h.2 ha
#align equiv.perm.is_cycle_on.range_zpow Equiv.Perm.IsCycleOn.range_zpow

theorem IsCycleOn.of_pow {n : ℕ} (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn f s s) : f.IsCycleOn s :=
  ⟨h, fun _ hx _ hy => (hf.2 hx hy).of_pow⟩
#align equiv.perm.is_cycle_on.of_pow Equiv.Perm.IsCycleOn.of_pow

theorem IsCycleOn.of_zpow {n : ℤ} (hf : (f ^ n).IsCycleOn s) (h : Set.BijOn f s s) :
    f.IsCycleOn s :=
  ⟨h, fun _ hx _ hy => (hf.2 hx hy).of_zpow⟩
#align equiv.perm.is_cycle_on.of_zpow Equiv.Perm.IsCycleOn.of_zpow

theorem IsCycleOn.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p)
    (h : g.IsCycleOn s) : (g.extendDomain f).IsCycleOn ((↑) ∘ f '' s) :=
  ⟨h.1.extendDomain, by
    rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
    exact (h.2 ha hb).extendDomain⟩
#align equiv.perm.is_cycle_on.extend_domain Equiv.Perm.IsCycleOn.extendDomain

protected theorem IsCycleOn.countable (hs : f.IsCycleOn s) : s.Countable := by
  obtain rfl | ⟨a, ha⟩ := s.eq_empty_or_nonempty
  · exact Set.countable_empty
  · exact (Set.countable_range fun n : ℤ => (⇑(f ^ n) : α → α) a).mono (hs.2 ha)
#align equiv.perm.is_cycle_on.countable Equiv.Perm.IsCycleOn.countable

end IsCycleOn

/-!
### `cycleOf`
-/


section CycleOf

variable [DecidableEq α] [Fintype α] {f g : Perm α} {x y : α}

/-- `f.cycleOf x` is the cycle of the permutation `f` to which `x` belongs. -/
def cycleOf (f : Perm α) (x : α) : Perm α :=
  ofSubtype (subtypePerm f fun _ => sameCycle_apply_right.symm : Perm { y // SameCycle f x y })
#align equiv.perm.cycle_of Equiv.Perm.cycleOf

theorem cycleOf_apply (f : Perm α) (x y : α) :
    cycleOf f x y = if SameCycle f x y then f y else y := by
  dsimp only [cycleOf]
  split_ifs with h
  · apply ofSubtype_apply_of_mem
    exact h
  · apply ofSubtype_apply_of_not_mem
    exact h
#align equiv.perm.cycle_of_apply Equiv.Perm.cycleOf_apply

theorem cycleOf_inv (f : Perm α) (x : α) : (cycleOf f x)⁻¹ = cycleOf f⁻¹ x :=
  Equiv.ext fun y => by
    rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
    split_ifs <;> simp_all [sameCycle_inv, sameCycle_inv_apply_right]
#align equiv.perm.cycle_of_inv Equiv.Perm.cycleOf_inv

@[simp]
theorem cycleOf_pow_apply_self (f : Perm α) (x : α) : ∀ n : ℕ, (cycleOf f x ^ n) x = (f ^ n) x := by
  intro n
  induction' n with n hn
  · rfl
  · rw [pow_succ, mul_apply, cycleOf_apply, hn, if_pos, pow_succ, mul_apply]
    simpa [SameCycle] using ⟨n,rfl⟩
#align equiv.perm.cycle_of_pow_apply_self Equiv.Perm.cycleOf_pow_apply_self

@[simp]
theorem cycleOf_zpow_apply_self (f : Perm α) (x : α) :
    ∀ n : ℤ, (cycleOf f x ^ n) x = (f ^ n) x := by
  intro z
  induction' z with z hz
  · exact cycleOf_pow_apply_self f x z
  · rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]
#align equiv.perm.cycle_of_zpow_apply_self Equiv.Perm.cycleOf_zpow_apply_self

theorem SameCycle.cycleOf_apply : SameCycle f x y → cycleOf f x y = f y :=
  ofSubtype_apply_of_mem _
#align equiv.perm.same_cycle.cycle_of_apply Equiv.Perm.SameCycle.cycleOf_apply

theorem cycleOf_apply_of_not_sameCycle : ¬SameCycle f x y → cycleOf f x y = y :=
  ofSubtype_apply_of_not_mem _
#align equiv.perm.cycle_of_apply_of_not_same_cycle Equiv.Perm.cycleOf_apply_of_not_sameCycle

theorem SameCycle.cycleOf_eq (h : SameCycle f x y) : cycleOf f x = cycleOf f y := by
  ext z
  rw [Equiv.Perm.cycleOf_apply]
  split_ifs with hz
  · exact (h.symm.trans hz).cycleOf_apply.symm
  · exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm
#align equiv.perm.same_cycle.cycle_of_eq Equiv.Perm.SameCycle.cycleOf_eq

@[simp]
theorem cycleOf_apply_apply_zpow_self (f : Perm α) (x : α) (k : ℤ) :
    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
  rw [SameCycle.cycleOf_apply]
  · rw [add_comm, zpow_add, zpow_one, mul_apply]
  · exact ⟨k, rfl⟩
#align equiv.perm.cycle_of_apply_apply_zpow_self Equiv.Perm.cycleOf_apply_apply_zpow_self

@[simp]
theorem cycleOf_apply_apply_pow_self (f : Perm α) (x : α) (k : ℕ) :
    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x := by
  convert cycleOf_apply_apply_zpow_self f x k using 1
#align equiv.perm.cycle_of_apply_apply_pow_self Equiv.Perm.cycleOf_apply_apply_pow_self

@[simp]
theorem cycleOf_apply_apply_self (f : Perm α) (x : α) : cycleOf f x (f x) = f (f x) := by
  convert cycleOf_apply_apply_pow_self f x 1 using 1
#align equiv.perm.cycle_of_apply_apply_self Equiv.Perm.cycleOf_apply_apply_self

@[simp]
theorem cycleOf_apply_self (f : Perm α) (x : α) : cycleOf f x x = f x :=
  SameCycle.rfl.cycleOf_apply
#align equiv.perm.cycle_of_apply_self Equiv.Perm.cycleOf_apply_self

theorem IsCycle.cycleOf_eq (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f :=
  Equiv.ext fun y =>
    if h : SameCycle f x y then by rw [h.cycleOf_apply]
    else by
      rw [cycleOf_apply_of_not_sameCycle h,
        Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]
#align equiv.perm.is_cycle.cycle_of_eq Equiv.Perm.IsCycle.cycleOf_eq

@[simp]
theorem cycleOf_eq_one_iff (f : Perm α) : cycleOf f x = 1 ↔ f x = x := by
  simp_rw [ext_iff, cycleOf_apply, one_apply]
  refine' ⟨fun h => (if_pos (SameCycle.refl f x)).symm.trans (h x), fun h y => _⟩
  by_cases hy : f y = y
  · rw [hy, ite_self]
  · exact if_neg (mt SameCycle.apply_eq_self_iff (by tauto))
#align equiv.perm.cycle_of_eq_one_iff Equiv.Perm.cycleOf_eq_one_iff

@[simp]
theorem cycleOf_self_apply (f : Perm α) (x : α) : cycleOf f (f x) = cycleOf f x :=
  (sameCycle_apply_right.2 SameCycle.rfl).symm.cycleOf_eq
#align equiv.perm.cycle_of_self_apply Equiv.Perm.cycleOf_self_apply

@[simp]
theorem cycleOf_self_apply_pow (f : Perm α) (n : ℕ) (x : α) : cycleOf f ((f ^ n) x) = cycleOf f x :=
  SameCycle.rfl.pow_left.cycleOf_eq
#align equiv.perm.cycle_of_self_apply_pow Equiv.Perm.cycleOf_self_apply_pow

@[simp]
theorem cycleOf_self_apply_zpow (f : Perm α) (n : ℤ) (x : α) :
    cycleOf f ((f ^ n) x) = cycleOf f x :=
  SameCycle.rfl.zpow_left.cycleOf_eq
#align equiv.perm.cycle_of_self_apply_zpow Equiv.Perm.cycleOf_self_apply_zpow

protected theorem IsCycle.cycleOf (hf : IsCycle f) : cycleOf f x = if f x = x then 1 else f := by
  by_cases hx : f x = x
  · rwa [if_pos hx, cycleOf_eq_one_iff]
  · rwa [if_neg hx, hf.cycleOf_eq]
#align equiv.perm.is_cycle.cycle_of Equiv.Perm.IsCycle.cycleOf

theorem cycleOf_one (x : α) : cycleOf 1 x = 1 :=
  (cycleOf_eq_one_iff 1).mpr rfl
#align equiv.perm.cycle_of_one Equiv.Perm.cycleOf_one

theorem isCycle_cycleOf (f : Perm α) (hx : f x ≠ x) : IsCycle (cycleOf f x) :=
  have : cycleOf f x x ≠ x := by rwa [SameCycle.rfl.cycleOf_apply]
  (isCycle_iff_sameCycle this).2 @fun y =>
    ⟨fun h => mt h.apply_eq_self_iff.2 this, fun h =>
      if hxy : SameCycle f x y then
        let ⟨i, hi⟩ := hxy
        ⟨i, by rw [cycleOf_zpow_apply_self, hi]⟩
      else by
        rw [cycleOf_apply_of_not_sameCycle hxy] at h
        exact (h rfl).elim⟩
#align equiv.perm.is_cycle_cycle_of Equiv.Perm.isCycle_cycleOf

@[simp]
theorem two_le_card_support_cycleOf_iff : 2 ≤ card (cycleOf f x).support ↔ f x ≠ x := by
  refine' ⟨fun h => _, fun h => by simpa using (isCycle_cycleOf _ h).two_le_card_support⟩
  contrapose! h
  rw [← cycleOf_eq_one_iff] at h
  simp [h]
#align equiv.perm.two_le_card_support_cycle_of_iff Equiv.Perm.two_le_card_support_cycleOf_iff

@[simp]
theorem card_support_cycleOf_pos_iff : 0 < card (cycleOf f x).support ↔ f x ≠ x := by
  rw [← two_le_card_support_cycleOf_iff, ← Nat.succ_le_iff]
  exact ⟨fun h => Or.resolve_left h.eq_or_lt (card_support_ne_one _).symm, zero_lt_two.trans_le⟩
#align equiv.perm.card_support_cycle_of_pos_iff Equiv.Perm.card_support_cycleOf_pos_iff

theorem pow_apply_eq_pow_mod_orderOf_cycleOf_apply (f : Perm α) (n : ℕ) (x : α) :
    (f ^ n) x = (f ^ (n % orderOf (cycleOf f x))) x := by
  rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_eq_mod_orderOf]
#align equiv.perm.pow_apply_eq_pow_mod_order_of_cycle_of_apply Equiv.Perm.pow_apply_eq_pow_mod_orderOf_cycleOf_apply

theorem cycleOf_mul_of_apply_right_eq_self (h : Commute f g) (x : α) (hx : g x = x) :
    (f * g).cycleOf x = f.cycleOf x := by
  ext y
  by_cases hxy : (f * g).SameCycle x y
  · obtain ⟨z, rfl⟩ := hxy
    rw [cycleOf_apply_apply_zpow_self]
    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
  · rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]
    contrapose! hxy
    obtain ⟨z, rfl⟩ := hxy
    refine' ⟨z, _⟩
    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
#align equiv.perm.cycle_of_mul_of_apply_right_eq_self Equiv.Perm.cycleOf_mul_of_apply_right_eq_self

theorem Disjoint.cycleOf_mul_distrib (h : f.Disjoint g) (x : α) :
    (f * g).cycleOf x = f.cycleOf x * g.cycleOf x := by
  cases' (disjoint_iff_eq_or_eq.mp h) x with hfx hgx
  · simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
  · simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]
#align equiv.perm.disjoint.cycle_of_mul_distrib Equiv.Perm.Disjoint.cycleOf_mul_distrib

theorem support_cycleOf_eq_nil_iff : (f.cycleOf x).support = ∅ ↔ x ∉ f.support := by simp
#align equiv.perm.support_cycle_of_eq_nil_iff Equiv.Perm.support_cycleOf_eq_nil_iff

theorem support_cycleOf_le (f : Perm α) (x : α) : support (f.cycleOf x) ≤ support f := by
  intro y hy
  rw [mem_support, cycleOf_apply] at hy
  split_ifs at hy
  · exact mem_support.mpr hy
  · exact absurd rfl hy
#align equiv.perm.support_cycle_of_le Equiv.Perm.support_cycleOf_le

theorem mem_support_cycleOf_iff : y ∈ support (f.cycleOf x) ↔ SameCycle f x y ∧ x ∈ support f := by
  by_cases hx : f x = x
  · rw [(cycleOf_eq_one_iff _).mpr hx]
    simp [hx]
  · rw [mem_support, cycleOf_apply]
    split_ifs with hy
    · simp only [hx, hy, iff_true_iff, Ne.def, not_false_iff, and_self_iff, mem_support]
      rcases hy with ⟨k, rfl⟩
      rw [← not_mem_support]
      simpa using hx
    · simpa [hx] using hy
#align equiv.perm.mem_support_cycle_of_iff Equiv.Perm.mem_support_cycleOf_iff

theorem mem_support_cycleOf_iff' (hx : f x ≠ x) : y ∈ support (f.cycleOf x) ↔ SameCycle f x y := by
  rw [mem_support_cycleOf_iff, and_iff_left (mem_support.2 hx)]
#align equiv.perm.mem_support_cycle_of_iff' Equiv.Perm.mem_support_cycleOf_iff'

theorem SameCycle.mem_support_iff (h : SameCycle f x y) : x ∈ support f ↔ y ∈ support f :=
  ⟨fun hx => support_cycleOf_le f x (mem_support_cycleOf_iff.mpr ⟨h, hx⟩), fun hy =>
    support_cycleOf_le f y (mem_support_cycleOf_iff.mpr ⟨h.symm, hy⟩)⟩
#align equiv.perm.same_cycle.mem_support_iff Equiv.Perm.SameCycle.mem_support_iff

theorem pow_mod_card_support_cycleOf_self_apply (f : Perm α) (n : ℕ) (x : α) :
    (f ^ (n % (f.cycleOf x).support.card)) x = (f ^ n) x := by
  by_cases hx : f x = x
  · rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]
  · rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
      ← pow_eq_mod_orderOf]
#align equiv.perm.pow_mod_card_support_cycle_of_self_apply Equiv.Perm.pow_mod_card_support_cycleOf_self_apply

/-- `x` is in the support of `f` iff `Equiv.Perm.cycle_of f x` is a cycle. -/
theorem isCycle_cycleOf_iff (f : Perm α) : IsCycle (cycleOf f x) ↔ f x ≠ x := by
  refine' ⟨fun hx => _, f.isCycle_cycleOf⟩
  rw [Ne.def, ← cycleOf_eq_one_iff f]
  exact hx.ne_one
#align equiv.perm.is_cycle_cycle_of_iff Equiv.Perm.isCycle_cycleOf_iff

theorem isCycleOn_support_cycleOf (f : Perm α) (x : α) : f.IsCycleOn (f.cycleOf x).support :=
  ⟨f.bijOn <| by
    refine fun _ ↦ ⟨fun h ↦ mem_support_cycleOf_iff.2 ?_, fun h ↦ mem_support_cycleOf_iff.2 ?_⟩
    · exact ⟨sameCycle_apply_right.1 (mem_support_cycleOf_iff.1 h).1,
      (mem_support_cycleOf_iff.1 h).2⟩
    · exact ⟨sameCycle_apply_right.2 (mem_support_cycleOf_iff.1 h).1,
      (mem_support_cycleOf_iff.1 h).2⟩
    , fun a ha b hb =>
      by
        rw [mem_coe, mem_support_cycleOf_iff] at ha hb
        exact ha.1.symm.trans hb.1⟩
#align equiv.perm.is_cycle_on_support_cycle_of Equiv.Perm.isCycleOn_support_cycleOf

theorem SameCycle.exists_pow_eq_of_mem_support (h : SameCycle f x y) (hx : x ∈ f.support) :
    ∃ (i : ℕ) (_ : i < (f.cycleOf x).support.card), (f ^ i) x = y := by
  rw [mem_support] at hx
  have := Equiv.Perm.IsCycleOn.exists_pow_eq (b := y) (f.isCycleOn_support_cycleOf x)
    (by rw [mem_support_cycleOf_iff' hx]) (by rwa [mem_support_cycleOf_iff' hx])
  simp_rw [← exists_prop] at this
  exact this
#align equiv.perm.same_cycle.exists_pow_eq_of_mem_support Equiv.Perm.SameCycle.exists_pow_eq_of_mem_support

theorem SameCycle.exists_pow_eq (f : Perm α) (h : SameCycle f x y) :
    ∃ (i : ℕ) (_ : 0 < i) (_ : i ≤ (f.cycleOf x).support.card + 1), (f ^ i) x = y := by
  by_cases hx : x ∈ f.support
  · obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
    cases' k with k
    · refine' ⟨(f.cycleOf x).support.card, _, self_le_add_right _ _, _⟩
      · refine' zero_lt_one.trans (one_lt_card_support_of_ne_one _)
        simpa using hx
      · simp only [Nat.zero_eq, pow_zero, coe_one, id_eq] at hk'
        subst hk'
        rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
          pow_orderOf_eq_one, one_apply]
    · exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩
  · refine' ⟨1, zero_lt_one, by simp, _⟩
    obtain ⟨k, rfl⟩ := h
    rw [not_mem_support] at hx
    rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]
#align equiv.perm.same_cycle.exists_pow_eq Equiv.Perm.SameCycle.exists_pow_eq

end CycleOf

/-!
### `cycleFactors`
-/


variable [DecidableEq α]

/-- Given a list `l : List α` and a permutation `f : perm α` whose nonfixed points are all in `l`,
  recursively factors `f` into cycles. -/
def cycleFactorsAux [Fintype α] :
    ∀ (l : List α) (f : Perm α),
      (∀ {x}, f x ≠ x → x ∈ l) →
        { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } := by
  intro l f h
  exact match l with
  | [] => ⟨[], by
      { simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true_iff,
          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *
        ext
        simp [*]}⟩
  | x::l =>
    if hx : f x = x then cycleFactorsAux l f (by
        intro y hy; exact List.mem_of_ne_of_mem (fun h => hy (by rwa [h])) (h hy))
    else
      let ⟨m, hm₁, hm₂, hm₃⟩ :=
        cycleFactorsAux l ((cycleOf f x)⁻¹ * f) (by
        intro y hy
        exact List.mem_of_ne_of_mem
            (fun h : y = x => by
              rw [h, mul_apply, Ne.def, inv_eq_iff_eq, cycleOf_apply_self] at hy
              exact hy rfl)
            (h fun h : f y = y => by
              rw [mul_apply, h, Ne.def, inv_eq_iff_eq, cycleOf_apply] at hy
              split_ifs at hy <;> tauto))
      ⟨cycleOf f x::m, by
        rw [List.prod_cons, hm₁]
        simp,
        fun g hg ↦ ((List.mem_cons).1 hg).elim (fun hg => hg.symm ▸ isCycle_cycleOf _ hx) (hm₂ g),
        List.pairwise_cons.2
          ⟨fun g hg y =>
            or_iff_not_imp_left.2 fun hfy =>
              have hxy : SameCycle f x y :=
                Classical.not_not.1 (mt cycleOf_apply_of_not_sameCycle hfy)
              have hgm : (g::m.erase g) ~ m :=
                List.cons_perm_iff_perm_erase.2 ⟨hg, List.Perm.refl _⟩
              have : ∀ h ∈ m.erase g, Disjoint g h :=
                (List.pairwise_cons.1
                    ((hgm.pairwise_iff fun a b (h : Disjoint a b) => h.symm).2 hm₃)).1
              by_cases id fun hgy : g y ≠ y =>
                (disjoint_prod_right _ this y).resolve_right <| by
                  have hsc : SameCycle f⁻¹ x (f y) := by
                    rwa [sameCycle_inv, sameCycle_apply_right]
                  rw [disjoint_prod_perm hm₃ hgm.symm, List.prod_cons,
                      ← eq_inv_mul_iff_mul_eq] at hm₁
                  rwa [hm₁, mul_apply, mul_apply, cycleOf_inv, hsc.cycleOf_apply, inv_apply_self,
                    inv_eq_iff_eq, eq_comm],
            hm₃⟩⟩
#align equiv.perm.cycle_factors_aux Equiv.Perm.cycleFactorsAux

theorem mem_list_cycles_iff {α : Type*} [Finite α] {l : List (Perm α)}
    (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle) (h2 : l.Pairwise Disjoint) {σ : Perm α} :
    σ ∈ l ↔ σ.IsCycle ∧ ∀ (a : α) (_ : σ a ≠ a), σ a = l.prod a := by
  suffices σ.IsCycle → (σ ∈ l ↔ ∀ (a : α) (_ : σ a ≠ a), σ a = l.prod a) by
    exact ⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩
  intro h3
  classical
    cases nonempty_fintype α
    constructor
    · intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
    · intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert hτ
      refine' h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key _ ha
      exact key a (mem_inter_of_mem ha hτa)
#align equiv.perm.mem_list_cycles_iff Equiv.Perm.mem_list_cycles_iff

theorem list_cycles_perm_list_cycles {α : Type*} [Finite α] {l₁ l₂ : List (Perm α)}
    (h₀ : l₁.prod = l₂.prod) (h₁l₁ : ∀ σ : Perm α, σ ∈ l₁ → σ.IsCycle)
    (h₁l₂ : ∀ σ : Perm α, σ ∈ l₂ → σ.IsCycle) (h₂l₁ : l₁.Pairwise Disjoint)
    (h₂l₂ : l₂.Pairwise Disjoint) : l₁ ~ l₂ := by
  classical
    refine'
      (List.perm_ext (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
            (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
        fun σ => _
    by_cases hσ : σ.IsCycle
    · obtain _ := not_forall.mp (mt ext hσ.ne_one)
      rw [mem_list_cycles_iff h₁l₁ h₂l₁, mem_list_cycles_iff h₁l₂ h₂l₂, h₀]
    · exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)
#align equiv.perm.list_cycles_perm_list_cycles Equiv.Perm.list_cycles_perm_list_cycles

/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`. -/
def cycleFactors [Fintype α] [LinearOrder α] (f : Perm α) :
    { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
  cycleFactorsAux (sort (α := α) (· ≤ ·) univ) f (fun {_ _} ↦ (mem_sort _).2 (mem_univ _))
#align equiv.perm.cycle_factors Equiv.Perm.cycleFactors

/-- Factors a permutation `f` into a list of disjoint cyclic permutations that multiply to `f`,
  without a linear order. -/
def truncCycleFactors [Fintype α] (f : Perm α) :
    Trunc { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } :=
  Quotient.recOnSubsingleton (@univ α _).1 (fun l h => Trunc.mk (cycleFactorsAux l f (h _)))
    (show ∀ x, f x ≠ x → x ∈ (@univ α _).1 from fun _ _ => mem_univ _)
#align equiv.perm.trunc_cycle_factors Equiv.Perm.truncCycleFactors

section CycleFactorsFinset

variable [Fintype α] (f : Perm α)

/-- Factors a permutation `f` into a `Finset` of disjoint cyclic permutations that multiply to `f`.
-/
def cycleFactorsFinset : Finset (Perm α) :=
  (truncCycleFactors f).lift
    (fun l : { l : List (Perm α) // l.prod = f ∧ (∀ g ∈ l, IsCycle g) ∧ l.Pairwise Disjoint } =>
      l.val.toFinset)
    fun ⟨_, hl⟩ ⟨_, hl'⟩ =>
    List.toFinset_eq_of_perm _ _
      (list_cycles_perm_list_cycles (hl'.left.symm ▸ hl.left) hl.right.left hl'.right.left
        hl.right.right hl'.right.right)
#align equiv.perm.cycle_factors_finset Equiv.Perm.cycleFactorsFinset

theorem cycleFactorsFinset_eq_list_toFinset {σ : Perm α} {l : List (Perm α)} (hn : l.Nodup) :
    σ.cycleFactorsFinset = l.toFinset ↔
      (∀ f : Perm α, f ∈ l → f.IsCycle) ∧ l.Pairwise Disjoint ∧ l.prod = σ := by
  obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors
  have ht : cycleFactorsFinset σ = l'.toFinset := by
    rw [cycleFactorsFinset, ← hl, Trunc.lift_mk]
  rw [ht]
  constructor
  · intro h
    have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
    have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
    refine' ⟨_, _, _⟩
    · exact fun _ h => hc' _ (hperm.subset h)
    · rwa [List.Perm.pairwise_iff Disjoint.symmetric hperm]
    · rw [← hp', hperm.symm.prod_eq']
      refine' hd'.imp _
      exact Disjoint.commute
  · rintro ⟨hc, hd, hp⟩
    refine' List.toFinset_eq_of_perm _ _ _
    refine' list_cycles_perm_list_cycles _ hc' hc hd' hd
    rw [hp, hp']
#align equiv.perm.cycle_factors_finset_eq_list_to_finset Equiv.Perm.cycleFactorsFinset_eq_list_toFinset

theorem cycleFactorsFinset_eq_finset {σ : Perm α} {s : Finset (Perm α)} :
    σ.cycleFactorsFinset = s ↔
      (∀ f : Perm α, f ∈ s → f.IsCycle) ∧
        ∃ h : (s : Set (Perm α)).Pairwise Disjoint,
          s.noncommProd id (h.mono' fun _ _ => Disjoint.commute) = σ := by
  obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq
  simp [cycleFactorsFinset_eq_list_toFinset, hl]
#align equiv.perm.cycle_factors_finset_eq_finset Equiv.Perm.cycleFactorsFinset_eq_finset

theorem cycleFactorsFinset_pairwise_disjoint :
    (cycleFactorsFinset f : Set (Perm α)).Pairwise Disjoint :=
  (cycleFactorsFinset_eq_finset.mp rfl).2.choose
#align equiv.perm.cycle_factors_finset_pairwise_disjoint Equiv.Perm.cycleFactorsFinset_pairwise_disjoint

theorem cycleFactorsFinset_mem_commute : (cycleFactorsFinset f : Set (Perm α)).Pairwise Commute :=
  (cycleFactorsFinset_pairwise_disjoint _).mono' fun _ _ => Disjoint.commute
#align equiv.perm.cycle_factors_finset_mem_commute Equiv.Perm.cycleFactorsFinset_mem_commute

/-- The product of cycle factors is equal to the original `f : perm α`. -/
theorem cycleFactorsFinset_noncommProd
    (comm : (cycleFactorsFinset f : Set (Perm α)).Pairwise Commute :=
      cycleFactorsFinset_mem_commute f) :
    f.cycleFactorsFinset.noncommProd id comm = f :=
  (cycleFactorsFinset_eq_finset.mp rfl).2.choose_spec
#align equiv.perm.cycle_factors_finset_noncomm_prod Equiv.Perm.cycleFactorsFinset_noncommProd

theorem mem_cycleFactorsFinset_iff {f p : Perm α} :
    p ∈ cycleFactorsFinset f ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a := by
  obtain ⟨l, hl, hl'⟩ := f.cycleFactorsFinset.exists_list_nodup_eq
  rw [← hl']
  rw [eq_comm, cycleFactorsFinset_eq_list_toFinset hl] at hl'
  simpa [List.mem_toFinset, Ne.def, ← hl'.right.right] using
    mem_list_cycles_iff hl'.left hl'.right.left
#align equiv.perm.mem_cycle_factors_finset_iff Equiv.Perm.mem_cycleFactorsFinset_iff

theorem cycleOf_mem_cycleFactorsFinset_iff {f : Perm α} {x : α} :
    cycleOf f x ∈ cycleFactorsFinset f ↔ x ∈ f.support := by
  rw [mem_cycleFactorsFinset_iff]
  constructor
  · rintro ⟨hc, _⟩
    contrapose! hc
    rw [not_mem_support, ← cycleOf_eq_one_iff] at hc
    simp [hc]
  · intro hx
    refine' ⟨isCycle_cycleOf _ (mem_support.mp hx), _⟩
    intro y hy
    rw [mem_support] at hy
    rw [cycleOf_apply]
    split_ifs with H
    · rfl
    · rw [cycleOf_apply_of_not_sameCycle H] at hy
      contradiction
#align equiv.perm.cycle_of_mem_cycle_factors_finset_iff Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff

theorem mem_cycleFactorsFinset_support_le {p f : Perm α} (h : p ∈ cycleFactorsFinset f) :
    p.support ≤ f.support := by
  rw [mem_cycleFactorsFinset_iff] at h
  intro x hx
  rwa [mem_support, ← h.right x hx, ← mem_support]
#align equiv.perm.mem_cycle_factors_finset_support_le Equiv.Perm.mem_cycleFactorsFinset_support_le

theorem cycleFactorsFinset_eq_empty_iff {f : Perm α} : cycleFactorsFinset f = ∅ ↔ f = 1 := by
  simpa [cycleFactorsFinset_eq_finset] using eq_comm
#align equiv.perm.cycle_factors_finset_eq_empty_iff Equiv.Perm.cycleFactorsFinset_eq_empty_iff

@[simp]
theorem cycleFactorsFinset_one : cycleFactorsFinset (1 : Perm α) = ∅ := by
  simp [cycleFactorsFinset_eq_empty_iff]
#align equiv.perm.cycle_factors_finset_one Equiv.Perm.cycleFactorsFinset_one

@[simp]
theorem cycleFactorsFinset_eq_singleton_self_iff {f : Perm α} :
    f.cycleFactorsFinset = {f} ↔ f.IsCycle := by simp [cycleFactorsFinset_eq_finset]
#align equiv.perm.cycle_factors_finset_eq_singleton_self_iff Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff

theorem IsCycle.cycleFactorsFinset_eq_singleton {f : Perm α} (hf : IsCycle f) :
    f.cycleFactorsFinset = {f} :=
  cycleFactorsFinset_eq_singleton_self_iff.mpr hf
#align equiv.perm.is_cycle.cycle_factors_finset_eq_singleton Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton

theorem cycleFactorsFinset_eq_singleton_iff {f g : Perm α} :
    f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g := by
  suffices f = g → (g.IsCycle ↔ f.IsCycle) by
    rw [cycleFactorsFinset_eq_finset]
    simpa [eq_comm]
  rintro rfl
  exact Iff.rfl
#align equiv.perm.cycle_factors_finset_eq_singleton_iff Equiv.Perm.cycleFactorsFinset_eq_singleton_iff

/-- Two permutations `f g : perm α` have the same cycle factors iff they are the same. -/
theorem cycleFactorsFinset_injective : Function.Injective (@cycleFactorsFinset α _ _) := by
  intro f g h
  rw [← cycleFactorsFinset_noncommProd f]
  simpa [h] using cycleFactorsFinset_noncommProd g
#align equiv.perm.cycle_factors_finset_injective Equiv.Perm.cycleFactorsFinset_injective

theorem Disjoint.disjoint_cycleFactorsFinset {f g : Perm α} (h : Disjoint f g) :
    _root_.Disjoint (cycleFactorsFinset f) (cycleFactorsFinset g) := by
  rw [disjoint_iff_disjoint_support] at h
  rw [Finset.disjoint_left]
  intro x hx hy
  simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy
  obtain ⟨⟨⟨a, ha, -⟩, hf⟩, -, hg⟩ := hx, hy
  have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)
  tauto
#align equiv.perm.disjoint.disjoint_cycle_factors_finset Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset

theorem Disjoint.cycleFactorsFinset_mul_eq_union {f g : Perm α} (h : Disjoint f g) :
    cycleFactorsFinset (f * g) = cycleFactorsFinset f ∪ cycleFactorsFinset g := by
  rw [cycleFactorsFinset_eq_finset]
  refine' ⟨_, _, _⟩
  · simp [or_imp, mem_cycleFactorsFinset_iff, forall_swap]
  · rw [coe_union, Set.pairwise_union_of_symmetric Disjoint.symmetric]
    exact
      ⟨cycleFactorsFinset_pairwise_disjoint _, cycleFactorsFinset_pairwise_disjoint _,
        fun x hx y hy _ =>
        h.mono (mem_cycleFactorsFinset_support_le hx) (mem_cycleFactorsFinset_support_le hy)⟩
  · rw [noncommProd_union_of_disjoint h.disjoint_cycleFactorsFinset]
    rw [cycleFactorsFinset_noncommProd, cycleFactorsFinset_noncommProd]
#align equiv.perm.disjoint.cycle_factors_finset_mul_eq_union Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union

theorem disjoint_mul_inv_of_mem_cycleFactorsFinset {f g : Perm α} (h : f ∈ cycleFactorsFinset g) :
    Disjoint (g * f⁻¹) f := by
  rw [mem_cycleFactorsFinset_iff] at h
  intro x
  by_cases hx : f x = x
  · exact Or.inr hx
  · refine' Or.inl _
    rw [mul_apply, ← h.right, apply_inv_self]
    rwa [← support_inv, apply_mem_support, support_inv, mem_support]
#align equiv.perm.disjoint_mul_inv_of_mem_cycle_factors_finset Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset

/-- If c is a cycle, a ∈ c.support and c is a cycle of f, then `c = f.cycleOf a` -/
theorem cycle_is_cycleOf {f c : Equiv.Perm α} {a : α} (ha : a ∈ c.support)
    (hc : c ∈ f.cycleFactorsFinset) : c = f.cycleOf a := by
  suffices f.cycleOf a = c.cycleOf a by
    rw [this]
    apply symm
    exact
      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
        (Equiv.Perm.mem_support.mp ha)
  let hfc := (Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset hc).symm
  let hfc2 := Perm.Disjoint.commute hfc
  rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]
  simp only [hfc2.eq, inv_mul_cancel_right]
  -- a est dans le support de c, donc pas dans celui de g c⁻¹
  exact
    Equiv.Perm.not_mem_support.mp
      (Finset.disjoint_left.mp (Equiv.Perm.Disjoint.disjoint_support hfc) ha)
#align equiv.perm.cycle_is_cycle_of Equiv.Perm.cycle_is_cycleOf

end CycleFactorsFinset

@[elab_as_elim]
theorem cycle_induction_on [Finite β] (P : Perm β → Prop) (σ : Perm β) (base_one : P 1)
    (base_cycles : ∀ σ : Perm β, σ.IsCycle → P σ)
    (induction_disjoint : ∀ σ τ : Perm β,
      Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)) : P σ := by
  cases nonempty_fintype β
  suffices ∀ l : List (Perm β),
      (∀ τ : Perm β, τ ∈ l → τ.IsCycle) → l.Pairwise Disjoint → P l.prod by
    classical
      let x := σ.truncCycleFactors.out
      exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
  intro l
  induction' l with σ l ih
  · exact fun _ _ => base_one
  · intro h1 h2
    rw [List.prod_cons]
    exact
      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
        (h1 _ (List.mem_cons_self _ _)) (base_cycles σ (h1 σ (l.mem_cons_self σ)))
        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)
#align equiv.perm.cycle_induction_on Equiv.Perm.cycle_induction_on

theorem cycleFactorsFinset_mul_inv_mem_eq_sdiff [Fintype α] {f g : Perm α}
    (h : f ∈ cycleFactorsFinset g) : cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f} := by
  revert f
  refine'
    cycle_induction_on (P := fun {g : Perm α} ↦
      ∀ {f}, (f ∈ cycleFactorsFinset g)
        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ _ _ _
  · simp
  · intro σ hσ f hf
    simp only [cycleFactorsFinset_eq_singleton_self_iff.mpr hσ, mem_singleton] at hf ⊢
    simp [hf]
  · intro σ τ hd _ hσ hτ f
    simp_rw [hd.cycleFactorsFinset_mul_eq_union, mem_union]
    -- if only `wlog` could work here...
    rintro (hf | hf)
    · rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
        erase_eq_of_not_mem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
      · rw [mem_cycleFactorsFinset_iff] at hf
        intro x
        cases' hd.symm x with hx hx
        · exact Or.inl hx
        · refine' Or.inr _
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction
      · exact fun H =>
        not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))
    · rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_not_mem, mul_assoc,
        Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]
      · rw [mem_cycleFactorsFinset_iff] at hf
        intro x
        cases' hd x with hx hx
        · exact Or.inl hx
        · refine' Or.inr _
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction
      · exact fun H =>
        not_mem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))
#align equiv.perm.cycle_factors_finset_mul_inv_mem_eq_sdiff Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff

section Generation

variable [Finite β]

open Subgroup

theorem closure_isCycle : closure { σ : Perm β | IsCycle σ } = ⊤ := by
  classical
    cases nonempty_fintype β
    exact
      top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))
#align equiv.perm.closure_is_cycle Equiv.Perm.closure_isCycle

variable [Fintype α]

theorem closure_cycle_adjacent_swap {σ : Perm α} (h1 : IsCycle σ) (h2 : σ.support = ⊤) (x : α) :
    closure ({σ, swap x (σ x)} : Set (Perm α)) = ⊤ := by
  let H := closure ({σ, swap x (σ x)} : Set (Perm α))
  have h3 : σ ∈ H := subset_closure (Set.mem_insert σ _)
  have h4 : swap x (σ x) ∈ H := subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
  have step1 : ∀ n : ℕ, swap ((σ ^ n) x) ((σ ^ (n + 1) : Perm α) x) ∈ H := by
    intro n
    induction' n with n ih
    · exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
    · convert H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
      simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ]
      rfl
  have step2 : ∀ n : ℕ, swap x ((σ ^ n) x) ∈ H := by
    intro n
    induction' n with n ih
    · simp only [Nat.zero_eq, pow_zero, coe_one, id_eq, swap_self, Set.mem_singleton_iff]
      convert H.one_mem
    · by_cases h5 : x = (σ ^ n) x
      · rw [pow_succ, mul_apply, ← h5]
        exact h4
      by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
      · rw [← h6, swap_self]
        exact H.one_mem
      rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]
      exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)
  have step3 : ∀ y : α, swap x y ∈ H := by
    intro y
    have hx : x ∈ (⊤ : Finset α) := Finset.mem_univ x
    rw [← h2, mem_support] at hx
    have hy : y ∈ (⊤ : Finset α) := Finset.mem_univ y
    rw [← h2, mem_support] at hy
    cases' IsCycle.exists_pow_eq h1 hx hy with n hn
    rw [← hn]
    exact step2 n
  have step4 : ∀ y z : α, swap y z ∈ H := by
    intro y z
    by_cases h5 : z = x
    · rw [h5, swap_comm]
      exact step3 y
    by_cases h6 : z = y
    · rw [h6, swap_self]
      exact H.one_mem
    rw [← swap_mul_swap_mul_swap h5 h6, swap_comm z x]
    exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)
  rw [eq_top_iff, ← closure_isSwap, closure_le]
  rintro τ ⟨y, z, _, h6⟩
  rw [h6]
  exact step4 y z
#align equiv.perm.closure_cycle_adjacent_swap Equiv.Perm.closure_cycle_adjacent_swap

theorem closure_cycle_coprime_swap {n : ℕ} {σ : Perm α} (h0 : Nat.Coprime n (Fintype.card α))
    (h1 : IsCycle σ) (h2 : σ.support = Finset.univ) (x : α) :
    closure ({σ, swap x ((σ ^ n) x)} : Set (Perm α)) = ⊤ := by
  rw [← Finset.card_univ, ← h2, ← h1.orderOf] at h0
  cases' exists_pow_eq_self_of_coprime h0 with m hm
  have h2' : (σ ^ n).support = ⊤ := Eq.trans (support_pow_coprime h0) h2
  have h1' : IsCycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1
  replace h1' : IsCycle (σ ^ n) :=
    h1'.of_pow (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm)))
  rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset_iff]
  exact
    ⟨Subgroup.pow_mem (closure _) (subset_closure (Set.mem_insert σ _)) n,
      Set.singleton_subset_iff.mpr (subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _)))⟩
#align equiv.perm.closure_cycle_coprime_swap Equiv.Perm.closure_cycle_coprime_swap

theorem closure_prime_cycle_swap {σ τ : Perm α} (h0 : (Fintype.card α).Prime) (h1 : IsCycle σ)
    (h2 : σ.support = Finset.univ) (h3 : IsSwap τ) : closure ({σ, τ} : Set (Perm α)) = ⊤ := by
  obtain ⟨x, y, h4, h5⟩ := h3
  obtain ⟨i, hi⟩ :=
    h1.exists_pow_eq (mem_support.mp ((Finset.ext_iff.mp h2 x).mpr (Finset.mem_univ x)))
      (mem_support.mp ((Finset.ext_iff.mp h2 y).mpr (Finset.mem_univ y)))
  rw [h5, ← hi]
  refine'
    closure_cycle_coprime_swap (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 _)) h1 h2 x
  cases' h with m hm
  rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi
#align equiv.perm.closure_prime_cycle_swap Equiv.Perm.closure_prime_cycle_swap

end Generation

section

variable [Fintype α] {σ τ : Perm α}

noncomputable section

theorem isConj_of_support_equiv
    (f : { x // x ∈ (σ.support : Set α) } ≃ { x // x ∈ (τ.support : Set α) })
    (hf :
      ∀ (x : α) (hx : x ∈ (σ.support : Set α)),
        (f ⟨σ x, apply_mem_support.2 hx⟩ : α) = τ ↑(f ⟨x, hx⟩)) :
    IsConj σ τ := by
  refine' isConj_iff.2 ⟨Equiv.extendSubtype f, _⟩
  rw [mul_inv_eq_iff_eq_mul]
  ext x
  simp only [Perm.mul_apply]
  by_cases hx : x ∈ σ.support
  · rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
    · exact hf x (Finset.mem_coe.2 hx)
  · rwa [Classical.not_not.1 ((not_congr mem_support).1 (Equiv.extendSubtype_not_mem f _ _)),
      Classical.not_not.1 ((not_congr mem_support).mp hx)]
#align equiv.perm.is_conj_of_support_equiv Equiv.Perm.isConj_of_support_equiv

theorem IsCycle.isConj (hσ : IsCycle σ) (hτ : IsCycle τ) (h : σ.support.card = τ.support.card) :
    IsConj σ τ := by
  refine'
    isConj_of_support_equiv
      (hσ.zpowersEquivSupport.symm.trans <|
        (zpowersEquivZpowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
      _
  intro x hx
  simp only [Perm.mul_apply, Equiv.trans_apply, Equiv.sumCongr_apply]
  obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
  apply
    Eq.trans _
      (congr rfl (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply n).symm))))
  apply (congr rfl (congr rfl (congr rfl (hσ.zpowersEquivSupport_symm_apply (n + 1))))).trans _
  simp only [Ne.def, IsCycle.zpowersEquivSupport_apply, Subtype.coe_mk,
    zpowersEquivZpowers_apply]
  dsimp
  rw [pow_succ, Perm.mul_apply]
#align equiv.perm.is_cycle.is_conj Equiv.Perm.IsCycle.isConj

theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) :
    IsConj σ τ ↔ σ.support.card = τ.support.card :=
  ⟨by
    intro h
    obtain ⟨π, rfl⟩ := (_root_.isConj_iff).1 h
    refine' Finset.card_congr (fun a _ => π a) (fun _ ha => _) (fun _ _ _ _ ab => π.injective ab)
        fun b hb => _
    · simp [mem_support.1 ha]
    · refine' ⟨π⁻¹ b, ⟨_, π.apply_inv_self b⟩⟩
      contrapose! hb
      rw [mem_support, Classical.not_not] at hb
      rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self],
    hσ.isConj hτ⟩
#align equiv.perm.is_cycle.is_conj_iff Equiv.Perm.IsCycle.isConj_iff

@[simp]
theorem support_conj : (σ * τ * σ⁻¹).support = τ.support.map σ.toEmbedding := by
  ext
  simp only [mem_map_equiv, Perm.coe_mul, Function.comp_apply, Ne.def, Perm.mem_support,
    Equiv.eq_symm_apply]
  rfl
#align equiv.perm.support_conj Equiv.Perm.support_conj

theorem card_support_conj : (σ * τ * σ⁻¹).support.card = τ.support.card := by simp
#align equiv.perm.card_support_conj Equiv.Perm.card_support_conj

end

theorem Disjoint.isConj_mul {α : Type*} [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π)
    (hc2 : IsConj τ ρ) (hd1 : Disjoint σ τ) (hd2 : Disjoint π ρ) : IsConj (σ * τ) (π * ρ) := by
  classical
    cases nonempty_fintype α
    obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
    obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
    have hd1' := coe_inj.2 hd1.support_mul
    have hd2' := coe_inj.2 hd2.support_mul
    rw [coe_union] at *
    have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
    have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
    refine' isConj_of_support_equiv _ _
    · refine'
          ((Equiv.Set.ofEq hd1').trans (Equiv.Set.union hd1''.le_bot)).trans
            ((Equiv.sumCongr (subtypeEquiv f fun a => _) (subtypeEquiv g fun a => _)).trans
              ((Equiv.Set.ofEq hd2').trans (Equiv.Set.union hd2''.le_bot)).symm) <;>
      · simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
          apply_eq_iff_eq]
    · intro x hx
      simp only [trans_apply, symm_trans_apply, Equiv.Set.ofEq_apply, Equiv.Set.ofEq_symm_apply,
        Equiv.sumCongr_apply]
      rw [hd1', Set.mem_union] at hx
      cases' hx with hxσ hxτ
      · rw [mem_coe, mem_support] at hxσ
        rw [Set.union_apply_left hd1''.le_bot _, Set.union_apply_left hd1''.le_bot _]
        simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
          Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq]
        · have h := (hd2 (f x)).resolve_left ?_
          · rw [mul_apply, mul_apply] at h
            rw [h, inv_apply_self, (hd1 x).resolve_left hxσ]
          · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
        · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
            apply_mem_support, mem_support]
        · rwa [Subtype.coe_mk, mem_coe, mem_support]
      · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
        rw [Set.union_apply_right hd1''.le_bot _, Set.union_apply_right hd1''.le_bot _]
        simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
          Set.union_symm_apply_right, Subtype.coe_mk, apply_eq_iff_eq]
        · have h := (hd2 (g (τ x))).resolve_right ?_
          · rw [mul_apply, mul_apply] at h
            rw [inv_apply_self, h, (hd1 (τ x)).resolve_right hxτ]
          · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
        · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
            mem_coe, mem_support]
        · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
#align equiv.perm.disjoint.is_conj_mul Equiv.Perm.Disjoint.isConj_mul

section FixedPoints

/-!
### Fixed points
-/


theorem fixed_point_card_lt_of_ne_one [Fintype α] {σ : Perm α} (h : σ ≠ 1) :
    (filter (fun x => σ x = x) univ).card < Fintype.card α - 1 := by
  rw [lt_tsub_iff_left, ← lt_tsub_iff_right, ← Finset.card_compl, Finset.compl_filter]
  exact one_lt_card_support_of_ne_one h
#align equiv.perm.fixed_point_card_lt_of_ne_one Equiv.Perm.fixed_point_card_lt_of_ne_one

end FixedPoints

end

open Equiv

namespace List

variable [DecidableEq α] {l : List α}

set_option linter.deprecated false in -- nthLe
theorem _root_.List.Nodup.isCycleOn_formPerm (h : l.Nodup) :
    l.formPerm.IsCycleOn { a | a ∈ l } := by
  refine' ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => _⟩
  rw [Set.mem_setOf, ← List.indexOf_lt_length] at ha hb
  rw [← List.indexOf_get ha, ← List.indexOf_get hb]
  refine' ⟨l.indexOf b - l.indexOf a, _⟩
  simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_ofNat,
    Equiv.Perm.coe_mul, ← List.nthLe_eq, List.formPerm_pow_apply_nthLe _ h, Function.comp]
  rw [add_comm]
#align list.nodup.is_cycle_on_form_perm List.Nodup.isCycleOn_formPerm

end List

namespace Int

open Equiv

theorem _root_.Int.addLeft_one_isCycle : (Equiv.addLeft 1 : Perm ℤ).IsCycle :=
  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩
#align int.add_left_one_is_cycle Int.addLeft_one_isCycle

theorem _root_.Int.addRight_one_isCycle : (Equiv.addRight 1 : Perm ℤ).IsCycle :=
  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩
#align int.add_right_one_is_cycle Int.addRight_one_isCycle

end Int

namespace Finset

variable [DecidableEq α] [Fintype α]

theorem _root_.Finset.exists_cycleOn (s : Finset α) :
    ∃ f : Perm α, f.IsCycleOn s ∧ f.support ⊆ s := by
  refine'
    ⟨s.toList.formPerm, _, fun x hx => by
      simpa using List.mem_of_formPerm_apply_ne _ _ (Perm.mem_support.1 hx)⟩
  convert s.nodup_toList.isCycleOn_formPerm
  simp
#align finset.exists_cycle_on Finset.exists_cycleOn

end Finset

namespace Set

variable {f : Perm α} {s : Set α}

theorem _root_.Set.Countable.exists_cycleOn (hs : s.Countable) :
    ∃ f : Perm α, f.IsCycleOn s ∧ { x | f x ≠ x } ⊆ s := by
  classical
    obtain hs' | hs' := s.finite_or_infinite
    · refine'
        ⟨hs'.toFinset.toList.formPerm, _, fun x hx => by
          simpa using List.mem_of_formPerm_apply_ne _ _ hx⟩
      convert hs'.toFinset.nodup_toList.isCycleOn_formPerm
      simp
    haveI := hs.to_subtype
    haveI := hs'.to_subtype
    obtain ⟨f⟩ : Nonempty (ℤ ≃ s) := inferInstance
    refine'
      ⟨(Equiv.addRight 1).extendDomain f, _, fun x hx =>
        of_not_not fun h => hx <| Perm.extendDomain_apply_not_subtype _ _ h⟩
    convert Int.addRight_one_isCycle.isCycleOn.extendDomain f
    rw [Set.image_comp, Equiv.image_eq_preimage]
    ext
    simp
#align set.countable.exists_cycle_on Set.Countable.exists_cycleOn

theorem _root_.Set.prod_self_eq_iUnion_perm (hf : f.IsCycleOn s) :
    s ×ˢ s = ⋃ n : ℤ, (fun a => (a, (f ^ n) a)) '' s := by
  ext ⟨a, b⟩
  simp only [Set.mem_prod, Set.mem_iUnion, Set.mem_image]
  refine' ⟨fun hx => _, _⟩
  · obtain ⟨n, rfl⟩ := hf.2 hx.1 hx.2
    exact ⟨_, _, hx.1, rfl⟩
  · rintro ⟨n, a, ha, ⟨⟩⟩
    exact ⟨ha, (hf.1.perm_zpow _).mapsTo ha⟩
#align set.prod_self_eq_Union_perm Set.prod_self_eq_iUnion_perm

end Set

namespace Finset

variable {f : Perm α} {s : Finset α}

theorem _root_.Finset.product_self_eq_disj_Union_perm_aux (hf : f.IsCycleOn s) :
    (range s.card : Set ℕ).PairwiseDisjoint fun k =>
      s.map ⟨fun i => (i, (f ^ k) i), fun i j => congr_arg Prod.fst⟩ := by
  obtain hs | _ := (s : Set α).subsingleton_or_nontrivial
  · refine' Set.Subsingleton.pairwise _ _
    simp_rw [Set.Subsingleton, mem_coe, ← card_le_one] at hs ⊢
    rwa [card_range]
  classical
    rintro m hm n hn hmn
    simp only [disjoint_left, Function.onFun, mem_map, Function.Embedding.coeFn_mk, exists_prop,
      not_exists, not_and, forall_exists_index, and_imp, Prod.forall, Prod.mk.inj_iff]
    rintro _ _ _ - rfl rfl a ha rfl h
    rw [hf.pow_apply_eq_pow_apply ha] at h
    rw [mem_coe, mem_range] at hm hn
    exact hmn.symm (h.eq_of_lt_of_lt hn hm)
#align finset.product_self_eq_disj_Union_perm_aux Finset.product_self_eq_disj_Union_perm_aux

/-- We can partition the square `s ×ˢ s` into shifted diagonals as such:
```
01234
40123
34012
23401
12340
```

The diagonals are given by the cycle `f`.
-/
theorem _root_.Finset.product_self_eq_disjUnion_perm (hf : f.IsCycleOn s) :
    s ×ˢ s =
      (range s.card).disjiUnion
        (fun k => s.map ⟨fun i => (i, (f ^ k) i), fun i j => congr_arg Prod.fst⟩)
        (product_self_eq_disj_Union_perm_aux hf) := by
  ext ⟨a, b⟩
  simp only [mem_product, Equiv.Perm.coe_pow, mem_disjiUnion, mem_range, mem_map,
    Function.Embedding.coeFn_mk, Prod.mk.inj_iff, exists_prop]
  refine' ⟨fun hx => _, _⟩
  · obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2
    exact ⟨n, hn, a, hx.1, rfl, by rw [f.iterate_eq_pow]⟩
  · rintro ⟨n, -, a, ha, rfl, rfl⟩
    exact ⟨ha, (hf.1.iterate _).mapsTo ha⟩
#align finset.product_self_eq_disj_Union_perm Finset.product_self_eq_disjUnionₓ_perm

end Finset

namespace Finset

variable [Semiring α] [AddCommMonoid β] [Module α β] {s : Finset ι} {σ : Perm ι}

theorem _root_.Finset.sum_smul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f : ι → α) (g : ι → β) :
    ((∑ i in s, f i) • ∑ i in s, g i) = ∑ k in range s.card, ∑ i in s, f i • g ((σ ^ k) i) := by
  simp_rw [sum_smul_sum, product_self_eq_disjUnion_perm hσ, sum_disjiUnion, sum_map]
  rfl
#align finset.sum_smul_sum_eq_sum_perm Finset.sum_smul_sum_eq_sum_perm

theorem _root_.Finset.sum_mul_sum_eq_sum_perm (hσ : σ.IsCycleOn s) (f g : ι → α) :
    ((∑ i in s, f i) * ∑ i in s, g i) = ∑ k in range s.card, ∑ i in s, f i * g ((σ ^ k) i) :=
  sum_smul_sum_eq_sum_perm hσ f g
#align finset.sum_mul_sum_eq_sum_perm Finset.sum_mul_sum_eq_sum_perm

end Finset
